Niech teraz będzie skończonym podzbiorem zbioru Możemy założyć, że Niech dalej będzie zbiorem tych elementów zbioru dla których występuje w Wówczas podkrata wyznaczona przez zbiór będąc skończenie generowaną kratą rozdzielną, jest skończona. Niech dalej będzie filtrem wyznaczonym przez w kracie Istnieje więc ideał pierwszy kraty który jest rozłączny z i zawiera Niech teraz Nietrudno wykazać, że spełnia wszystkie formuły ze zbioru Wobec dowolności zbioru oznacza to, że każdy skończony podzbiór zbioru jest spełnialny. Niech zatem spełnia wszystkie formuły zbioru Wówczas jest szukanym ideałem pierwszym kraty
Uwagi i wnioski Dowód twierdzenia o ideale pierwszym zaliczany jest do tzw. dowodów niekonstruktywnych, czyli, w uproszczeniu, wykorzystujących pewne formy aksjomatu wyboru (AC). W tym wypadku, w dowodzie najczęściej korzysta się z lematu Kuratowskiego-Zorna. Chociaż na gruncie teorii mnogości Zermela-Fraenkla BPI jest słabsze od pewnika wyboru (tzn.