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 )
consider y being Element of L such that
A3: y is_a_complement_of x by WAYBEL_1:def 24;
x "/\" y = Bottom L by A3;
then x "/\" y <= l by YELLOW_0:44;
then A4: ( x <= l or y <= l ) by A2;
assume x > l ; :: thesis: x = Top L
then y < x by A4, ORDERS_2:7;
then A5: y <= x by ORDERS_2:def 6;
x "\/" y = Top L by A3;
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 x "/\" y <= l ; :: thesis: ( x <= l or y <= l )
then A7: l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ;
assume that
A8: not x <= l and
A9: not y <= l ; :: thesis: contradiction
A10: l <> l "\/" y by A9, YELLOW_0:24;
l <= l "\/" y by A7, YELLOW_0:23;
then l < l "\/" y by A10, ORDERS_2:def 6;
then A11: l "\/" y = Top L by A6;
A12: l <> l "\/" x by A8, YELLOW_0:24;
l <= l "\/" x by A7, YELLOW_0:23;
then l < l "\/" x by A12, ORDERS_2:def 6;
then l "\/" x = Top L by A6;
hence contradiction by A1, A7, A11, YELLOW_5:2; :: thesis: verum
end;