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 )

proof

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}

proof

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;

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

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;

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;

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;

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

then ( z "/\" y <= z & z <= l ) by A2, YELLOW_0:23;
then A13: z "/\" y <= l by ORDERS_2:3;
thus (f . z) "/\" (f . y) = {} /\ {x} by A12, YELLOW_1:17
.= f . (z "/\" y) by A2, A13 ; :: thesis: verum

end;

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

then ( z "/\" y <= y & y <= l ) by A2, YELLOW_0:23;
then A15: z "/\" y <= l by ORDERS_2:3;
thus (f . z) "/\" (f . y) = {x} /\ {} by A14, YELLOW_1:17
.= f . (z "/\" y) by A2, A15 ; :: thesis: verum

end;

end;

end;

inf (f .: {z,y}) = (f . z) "/\" (f . y) by A5, YELLOW_0:40
.= f . (inf {z,y}) by A7, YELLOW_0:40 ;
hence f preserves_inf_of {z,y} by A6; :: thesis: verum

end;

hence f is meet-preserving ; :: thesis: f is join-preserving
for z, y being Element of L holds f preserves_sup_of {z,y}

proof

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;

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

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;

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;

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;

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;

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;

end;

end;

sup (f .: {z,y}) = (f . z) "\/" (f . y) by A16, YELLOW_0:41
.= f . (sup {z,y}) by A18, YELLOW_0:41 ;
hence f preserves_sup_of {z,y} by A17; :: thesis: verum

end;

hence f is join-preserving ; :: thesis: verum

end;

thus ( ( 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 ) :: thesis: verum

proof

defpred S₁[ 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₁[a,b]

proof

let a be Element of L; :: thesis: ex b being Element of (BoolePoset {{}}) st S₁[a,b]

now :: thesis: ex b being Element of (BoolePoset {{}}) st S₁[a,b]

per cases ( a <= l or not a <= l ) ;

suppose A30: a <= l ; :: thesis: ex b being Element of (BoolePoset {{}}) st S₁[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₁[a,b] ; :: thesis: verum

end;

suppose A31: not a <= l ; :: thesis: ex b being Element of (BoolePoset {{}}) st S₁[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₁[a,b] ; :: thesis: verum

end;

end;

end;

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

end;

consider f being Function of L,(BoolePoset {{}}) such that
A32: for p being Element of L holds S₁[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 ;

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

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

hence ( z <= l or y <= l ) by A32; :: thesis: verum

end;