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,() 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,() 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,() 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,() 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,() 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,() 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,(); :: 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 () = the carrier of (InclPoset ()) 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:
A5: f .: {z,y} = {(f . z),(f . y)} by ;
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 ;
suppose A8: ( f . z = {} & f . y = {} ) ; :: thesis: (f . z) "/\" (f . y) = f . (z "/\" y)
then ( z "/\" y <= z & z <= l ) by ;
then A9: z "/\" y <= l by ORDERS_2:3;
thus (f . z) "/\" (f . y) = {} /\ {} by
.= 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
.= f . (z "/\" y) by ; :: 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 ;
then A13: z "/\" y <= l by ORDERS_2:3;
thus (f . z) "/\" (f . y) = {} /\ {x} by
.= f . (z "/\" y) by ; :: 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 ;
then A15: z "/\" y <= l by ORDERS_2:3;
thus (f . z) "/\" (f . y) = {x} /\ {} by
.= f . (z "/\" y) by ; :: thesis: verum
end;
end;
end;
inf (f .: {z,y}) = (f . z) "/\" (f . y) by
.= f . (inf {z,y}) by ;
hence f preserves_inf_of {z,y} by A6; :: thesis: verum
end;
hence f is meet-preserving ; :: thesis:
for z, y being Element of L holds f preserves_sup_of {z,y}
proof
let z, y be Element of L; :: thesis:
A16: f .: {z,y} = {(f . z),(f . y)} by ;
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 ;
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
.= f . (z "\/" y) by ; :: 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 ;
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
.= f . (z "\/" y) by ; :: 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 ;
then not z "\/" y <= l by ORDERS_2:3;
then A24: not f . (z "\/" y) = {} by A2;
thus (f . z) "\/" (f . y) = {} \/ {x} by
.= f . (z "\/" y) by ; :: 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 ;
then not z "\/" y <= l by ORDERS_2:3;
then A26: not f . (z "\/" y) = {} by A2;
thus (f . z) "\/" (f . y) = {x} \/ {} by
.= f . (z "\/" y) by ; :: thesis: verum
end;
end;
end;
sup (f .: {z,y}) = (f . z) "\/" (f . y) by
.= f . (sup {z,y}) by ;
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,() 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 S1[ Element of L, set ] means ( \$1 <= l iff \$2 = {} );
assume A27: for x being set
for f being Function of L,() 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 = the carrier of () 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 st S1[a,b]
proof
let a be Element of L; :: thesis: ex b being Element of st S1[a,b]
now :: thesis: ex b being Element of st S1[a,b]
per cases ( a <= l or not a <= l ) ;
suppose A30: a <= l ; :: thesis: ex b being Element of st S1[a,b]
set b = {} ;
reconsider b = {} as Element of by ;
( a <= l iff b = {} ) by A30;
hence ex b being Element of st S1[a,b] ; :: thesis: verum
end;
suppose A31: not a <= l ; :: thesis: ex b being Element of st S1[a,b]
set b = ;
reconsider b = as Element of by ;
( a <= l iff b = {} ) by A31;
hence ex b being Element of st S1[a,b] ; :: thesis: verum
end;
end;
end;
hence ex b being Element of st S1[a,b] ; :: thesis: verum
end;
consider f being Function of L, such that
A32: for p being Element of L holds S1[p,f . p] from f is meet-preserving by ;
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
.= (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 ;
hence contradiction by A35; :: thesis: verum
end;
hence ( z <= l or y <= l ) by A32; :: thesis: verum
end;