then consider a being object such that A1:
( a in I & not a inmeet { P where P is Ideal of L : ( P is prime & I c= P ) } )
; consider Y being set such that X4:
( Y in { P where P is Ideal of L : ( P is prime & I c= P ) } & not a in Y )
bySETFAM_1:def 1, A1, k1; consider P1 being Ideal of L such that X5:
( Y = P1 & P1 is prime & I c= P1 )
byX4; thus
contradiction
byA1, X4, X5; :: thesis: verum