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 )

x = Top L ) implies l is prime ) :: thesis: verum

( 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

thus
( ( for x being Element of L st x > l holds
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;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

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;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