let L be Boolean LATTICE; :: thesis: for l being Element of L st l <> Top L holds
( l is prime iff for x being Element of L st x > l holds
x = Top L )
let l be Element of L; :: thesis: ( l <> Top L implies ( l is prime iff for x being Element of L st x > l holds
x = Top L ) )
assume A1: l <> Top L ; :: thesis: ( l is prime iff for x being Element of L st x > l holds
x = Top L )
thus ( l is prime implies for x being Element of L st x > l holds
x = Top L ) :: thesis: ( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime )

proof

assume A2: l is prime ; :: thesis: for x being Element of L st x > l holds
x = Top L
let x be Element of L; :: thesis: ( x > l implies x = Top L )
assume A3: x > l ; :: thesis: x = Top L
consider y being Element of L such that
A4: y is_a_complement_of x by WAYBEL_1:def 24;
A5: ( x "\/" y = Top L & x "/\" y = Bottom L ) by A4, WAYBEL_1:def 23;
then x "/\" y <= l by YELLOW_0:44;
then ( x <= l or y <= l ) by A2, Def6;
then y < x by A3, ORDERS_2:32;
then y <= x by ORDERS_2:def 10;
hence x = Top L by A5, YELLOW_0:24; :: thesis: verum

end;

thus ( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime ) :: thesis: verum

proof

assume A6: for z being Element of L st z > l holds
z = Top L ; :: thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume A7: x "/\" y <= l ; :: thesis: ( x <= l or y <= l )
assume A8: ( not x <= l & not y <= l ) ; :: thesis: contradiction
A9: l = l "\/" (x "/\" y) by A7, YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:6 ;
then A10: ( l <= l "\/" x & l <= l "\/" y ) by YELLOW_0:23;
l <> l "\/" x by A8, YELLOW_0:24;
then l < l "\/" x by A10, ORDERS_2:def 10;
then A11: l "\/" x = Top L by A6;
l <> l "\/" y by A8, YELLOW_0:24;
then l < l "\/" y by A10, ORDERS_2:def 10;
then l "\/" y = Top L by A6;
hence contradiction by A1, A9, A11, YELLOW_5:2; :: thesis: verum

end;