let L be Boolean LATTICE; 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; ( 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
; ( 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 )
( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime )
thus
( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime )
verumproof
assume A6:
for
z being
Element of
L st
z > l holds
z = Top L
;
l is prime
let x,
y be
Element of
L;
WAYBEL_6:def 6 ( not x "/\" y <= l or x <= l or y <= l )
assume
x "/\" y <= l
;
( 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
;
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;
verum
end;