let L be LATTICE; :: thesis: for l being Element of L holds

( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

let l be Element of L; :: thesis: ( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

thus ( l is prime implies for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) :: thesis: ( ( for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) implies l is prime )

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) implies l is prime ) :: thesis: verum

( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

let l be Element of L; :: thesis: ( l is prime iff for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) )

thus ( l is prime implies for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) :: thesis: ( ( for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) implies l is prime )

proof

thus
( ( for x being set
assume A1:
l is prime
; :: thesis: for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving )

let x be set ; :: thesis: for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving )

let f be Function of L,(BoolePoset {x}); :: thesis: ( ( for p being Element of L holds

( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) )

assume A2: for p being Element of L holds

( f . p = {} iff p <= l ) ; :: thesis: ( f is meet-preserving & f is join-preserving )

A3: the carrier of (BoolePoset {x}) = the carrier of (InclPoset (bool {x})) by YELLOW_1:4

.= bool {x} by YELLOW_1:1

.= {{},{x}} by ZFMISC_1:24 ;

A4: dom f = the carrier of L by FUNCT_2:def 1;

for z, y being Element of L holds f preserves_inf_of {z,y}

for z, y being Element of L holds f preserves_sup_of {z,y}

end;for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving )

let x be set ; :: thesis: for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving )

let f be Function of L,(BoolePoset {x}); :: thesis: ( ( for p being Element of L holds

( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) )

assume A2: for p being Element of L holds

( f . p = {} iff p <= l ) ; :: thesis: ( f is meet-preserving & f is join-preserving )

A3: the carrier of (BoolePoset {x}) = the carrier of (InclPoset (bool {x})) by YELLOW_1:4

.= bool {x} by YELLOW_1:1

.= {{},{x}} by ZFMISC_1:24 ;

A4: dom f = the carrier of L by FUNCT_2:def 1;

for z, y being Element of L holds f preserves_inf_of {z,y}

proof

hence
f is meet-preserving
; :: thesis: f is join-preserving
let z, y be Element of L; :: thesis: f preserves_inf_of {z,y}

A5: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60;

then A6: ( ex_inf_of {z,y},L implies ex_inf_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:21;

.= f . (inf {z,y}) by A7, YELLOW_0:40 ;

hence f preserves_inf_of {z,y} by A6; :: thesis: verum

end;A5: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60;

then A6: ( ex_inf_of {z,y},L implies ex_inf_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:21;

A7: now :: thesis: (f . z) "/\" (f . y) = f . (z "/\" y)end;

inf (f .: {z,y}) =
(f . z) "/\" (f . y)
by A5, YELLOW_0:40
per cases
( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) )
by A3, TARSKI:def 2;

end;

suppose A8:
( f . z = {} & f . y = {} )
; :: thesis: (f . z) "/\" (f . y) = f . (z "/\" y)

then
( z "/\" y <= z & z <= l )
by A2, YELLOW_0:23;

then A9: z "/\" y <= l by ORDERS_2:3;

thus (f . z) "/\" (f . y) = {} /\ {} by A8, YELLOW_1:17

.= f . (z "/\" y) by A2, A9 ; :: thesis: verum

end;then A9: z "/\" y <= l by ORDERS_2:3;

thus (f . z) "/\" (f . y) = {} /\ {} by A8, YELLOW_1:17

.= f . (z "/\" y) by A2, A9 ; :: thesis: verum

suppose A10:
( f . z = {x} & f . y = {x} )
; :: thesis: (f . z) "/\" (f . y) = f . (z "/\" y)

then
( not y <= l & not z <= l )
by A2;

then not z "/\" y <= l by A1;

then A11: not f . (z "/\" y) = {} by A2;

thus (f . z) "/\" (f . y) = {x} /\ {x} by A10, YELLOW_1:17

.= f . (z "/\" y) by A3, A11, TARSKI:def 2 ; :: thesis: verum

end;then not z "/\" y <= l by A1;

then A11: not f . (z "/\" y) = {} by A2;

thus (f . z) "/\" (f . y) = {x} /\ {x} by A10, YELLOW_1:17

.= f . (z "/\" y) by A3, A11, TARSKI:def 2 ; :: thesis: verum

.= f . (inf {z,y}) by A7, YELLOW_0:40 ;

hence f preserves_inf_of {z,y} by A6; :: thesis: verum

for z, y being Element of L holds f preserves_sup_of {z,y}

proof

hence
f is join-preserving
; :: thesis: verum
let z, y be Element of L; :: thesis: f preserves_sup_of {z,y}

A16: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60;

then A17: ( ex_sup_of {z,y},L implies ex_sup_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:20;

.= f . (sup {z,y}) by A18, YELLOW_0:41 ;

hence f preserves_sup_of {z,y} by A17; :: thesis: verum

end;A16: f .: {z,y} = {(f . z),(f . y)} by A4, FUNCT_1:60;

then A17: ( ex_sup_of {z,y},L implies ex_sup_of f .: {z,y}, BoolePoset {x} ) by YELLOW_0:20;

A18: now :: thesis: (f . z) "\/" (f . y) = f . (z "\/" y)end;

sup (f .: {z,y}) =
(f . z) "\/" (f . y)
by A16, YELLOW_0:41
per cases
( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) )
by A3, TARSKI:def 2;

end;

suppose A19:
( f . z = {} & f . y = {} )
; :: thesis: (f . z) "\/" (f . y) = f . (z "\/" y)

then
( z <= l & y <= l )
by A2;

then A20: z "\/" y <= l by YELLOW_0:22;

thus (f . z) "\/" (f . y) = {} \/ {} by A19, YELLOW_1:17

.= f . (z "\/" y) by A2, A20 ; :: thesis: verum

end;then A20: z "\/" y <= l by YELLOW_0:22;

thus (f . z) "\/" (f . y) = {} \/ {} by A19, YELLOW_1:17

.= f . (z "\/" y) by A2, A20 ; :: thesis: verum

suppose A21:
( f . z = {x} & f . y = {x} )
; :: thesis: (f . z) "\/" (f . y) = f . (z "\/" y)

then
( z "\/" y >= z & not z <= l )
by A2, YELLOW_0:22;

then not z "\/" y <= l by ORDERS_2:3;

then A22: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {x} \/ {x} by A21, YELLOW_1:17

.= f . (z "\/" y) by A3, A22, TARSKI:def 2 ; :: thesis: verum

end;then not z "\/" y <= l by ORDERS_2:3;

then A22: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {x} \/ {x} by A21, YELLOW_1:17

.= f . (z "\/" y) by A3, A22, TARSKI:def 2 ; :: thesis: verum

suppose A23:
( f . z = {} & f . y = {x} )
; :: thesis: (f . z) "\/" (f . y) = f . (z "\/" y)

then
( z "\/" y >= y & not y <= l )
by A2, YELLOW_0:22;

then not z "\/" y <= l by ORDERS_2:3;

then A24: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {} \/ {x} by A23, YELLOW_1:17

.= f . (z "\/" y) by A3, A24, TARSKI:def 2 ; :: thesis: verum

end;then not z "\/" y <= l by ORDERS_2:3;

then A24: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {} \/ {x} by A23, YELLOW_1:17

.= f . (z "\/" y) by A3, A24, TARSKI:def 2 ; :: thesis: verum

suppose A25:
( f . z = {x} & f . y = {} )
; :: thesis: (f . z) "\/" (f . y) = f . (z "\/" y)

then
( z "\/" y >= z & not z <= l )
by A2, YELLOW_0:22;

then not z "\/" y <= l by ORDERS_2:3;

then A26: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {x} \/ {} by A25, YELLOW_1:17

.= f . (z "\/" y) by A3, A26, TARSKI:def 2 ; :: thesis: verum

end;then not z "\/" y <= l by ORDERS_2:3;

then A26: not f . (z "\/" y) = {} by A2;

thus (f . z) "\/" (f . y) = {x} \/ {} by A25, YELLOW_1:17

.= f . (z "\/" y) by A3, A26, TARSKI:def 2 ; :: thesis: verum

.= f . (sup {z,y}) by A18, YELLOW_0:41 ;

hence f preserves_sup_of {z,y} by A17; :: thesis: verum

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ) implies l is prime ) :: thesis: verum

proof

defpred S_{1}[ Element of L, set ] means ( $1 <= l iff $2 = {} );

assume A27: for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ; :: thesis: l is prime

let z, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not z "/\" y <= l or z <= l or y <= l )

A28: the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4

.= bool {{}} by YELLOW_1:1

.= {{},{{}}} by ZFMISC_1:24 ;

A29: for a being Element of L ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]

A32: for p being Element of L holds S_{1}[p,f . p]
from FUNCT_2:sch 3(A29);

f is meet-preserving by A27, A32;

then A33: ( ex_inf_of {z,y},L & f preserves_inf_of {z,y} ) by YELLOW_0:21;

dom f = the carrier of L by FUNCT_2:def 1;

then A34: f .: {z,y} = {(f . z),(f . y)} by FUNCT_1:60;

assume z "/\" y <= l ; :: thesis: ( z <= l or y <= l )

then A35: {} = f . (z "/\" y) by A32

.= f . (inf {z,y}) by YELLOW_0:40

.= inf {(f . z),(f . y)} by A34, A33

.= (f . z) "/\" (f . y) by YELLOW_0:40

.= (f . z) /\ (f . y) by YELLOW_1:17 ;

end;assume A27: for x being set

for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds

( f . p = {} iff p <= l ) ) holds

( f is meet-preserving & f is join-preserving ) ; :: thesis: l is prime

let z, y be Element of L; :: according to WAYBEL_6:def 6 :: thesis: ( not z "/\" y <= l or z <= l or y <= l )

A28: the carrier of (BoolePoset {{}}) = the carrier of (InclPoset (bool {{}})) by YELLOW_1:4

.= bool {{}} by YELLOW_1:1

.= {{},{{}}} by ZFMISC_1:24 ;

A29: for a being Element of L ex b being Element of (BoolePoset {{}}) st S

proof

consider f being Function of L,(BoolePoset {{}}) such that
let a be Element of L; :: thesis: ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]

_{1}[a,b]
; :: thesis: verum

end;now :: thesis: ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]end;

hence
ex b being Element of (BoolePoset {{}}) st Sper cases
( a <= l or not a <= l )
;

end;

suppose A30:
a <= l
; :: thesis: ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]

set b = {} ;

reconsider b = {} as Element of (BoolePoset {{}}) by A28, TARSKI:def 2;

( a <= l iff b = {} ) by A30;

hence ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]
; :: thesis: verum

end;reconsider b = {} as Element of (BoolePoset {{}}) by A28, TARSKI:def 2;

( a <= l iff b = {} ) by A30;

hence ex b being Element of (BoolePoset {{}}) st S

suppose A31:
not a <= l
; :: thesis: ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]

set b = {{}};

reconsider b = {{}} as Element of (BoolePoset {{}}) by A28, TARSKI:def 2;

( a <= l iff b = {} ) by A31;

hence ex b being Element of (BoolePoset {{}}) st S_{1}[a,b]
; :: thesis: verum

end;reconsider b = {{}} as Element of (BoolePoset {{}}) by A28, TARSKI:def 2;

( a <= l iff b = {} ) by A31;

hence ex b being Element of (BoolePoset {{}}) st S

A32: for p being Element of L holds S

f is meet-preserving by A27, A32;

then A33: ( ex_inf_of {z,y},L & f preserves_inf_of {z,y} ) by YELLOW_0:21;

dom f = the carrier of L by FUNCT_2:def 1;

then A34: f .: {z,y} = {(f . z),(f . y)} by FUNCT_1:60;

assume z "/\" y <= l ; :: thesis: ( z <= l or y <= l )

then A35: {} = f . (z "/\" y) by A32

.= f . (inf {z,y}) by YELLOW_0:40

.= inf {(f . z),(f . y)} by A34, A33

.= (f . z) "/\" (f . y) by YELLOW_0:40

.= (f . z) /\ (f . y) by YELLOW_1:17 ;

now :: thesis: ( not f . z = {} implies f . y = {} )

hence
( z <= l or y <= l )
by A32; :: thesis: verumassume
( not f . z = {} & not f . y = {} )
; :: thesis: contradiction

then ( f . z = {{}} & f . y = {{}} ) by A28, TARSKI:def 2;

hence contradiction by A35; :: thesis: verum

end;then ( f . z = {{}} & f . y = {{}} ) by A28, TARSKI:def 2;

hence contradiction by A35; :: thesis: verum