let L be complete LATTICE; :: thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) )

set H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;

set p9 = the prime Element of L;

A1: chi (((downarrow the prime Element of L) `), the carrier of L) in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;

deffunc H_{1}( object ) -> set = { f where f is Element of H : f . $1 = 1 } ;

consider F being Function such that

A2: dom F = the carrier of L and

A3: for x being object st x in the carrier of L holds

F . x = H_{1}(x)
from FUNCT_1:sch 3();

A4: the carrier of (BoolePoset H) = the carrier of (InclPoset (bool H)) by YELLOW_1:4

.= bool H by YELLOW_1:1 ;

rng F c= the carrier of (BoolePoset H)

A7: F is meet-preserving

A29: F is V27()

F is sups-preserving

set H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;

set p9 = the prime Element of L;

A1: chi (((downarrow the prime Element of L) `), the carrier of L) in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;

now :: thesis: for x being object st x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } holds

x is Function

then reconsider H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } as non empty functional set by A1, FUNCT_1:def 13;x is Function

let x be object ; :: thesis: ( x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } implies x is Function )

assume x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; :: thesis: x is Function

then ex p being Element of L st

( x = chi (((downarrow p) `), the carrier of L) & p is prime ) ;

hence x is Function ; :: thesis: verum

end;assume x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; :: thesis: x is Function

then ex p being Element of L st

( x = chi (((downarrow p) `), the carrier of L) & p is prime ) ;

hence x is Function ; :: thesis: verum

deffunc H

consider F being Function such that

A2: dom F = the carrier of L and

A3: for x being object st x in the carrier of L holds

F . x = H

A4: the carrier of (BoolePoset H) = the carrier of (InclPoset (bool H)) by YELLOW_1:4

.= bool H by YELLOW_1:1 ;

rng F c= the carrier of (BoolePoset H)

proof

then reconsider F = F as Function of L,(BoolePoset H) by A2, FUNCT_2:def 1, RELSET_1:4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in the carrier of (BoolePoset H) )

reconsider yy = y as set by TARSKI:1;

assume y in rng F ; :: thesis: y in the carrier of (BoolePoset H)

then consider x being object such that

A5: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

A6: y = { f where f is Element of H : f . x = 1 } by A2, A3, A5;

yy c= H

end;reconsider yy = y as set by TARSKI:1;

assume y in rng F ; :: thesis: y in the carrier of (BoolePoset H)

then consider x being object such that

A5: ( x in dom F & y = F . x ) by FUNCT_1:def 3;

A6: y = { f where f is Element of H : f . x = 1 } by A2, A3, A5;

yy c= H

proof

hence
y in the carrier of (BoolePoset H)
by A4; :: thesis: verum
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in yy or p in H )

assume p in yy ; :: thesis: p in H

then ex f being Element of H st

( p = f & f . x = 1 ) by A6;

hence p in H ; :: thesis: verum

end;assume p in yy ; :: thesis: p in H

then ex f being Element of H st

( p = f & f . x = 1 ) by A6;

hence p in H ; :: thesis: verum

A7: F is meet-preserving

proof

assume A28:
PRIME L is order-generating
; :: thesis: ( L is distributive & L is meet-continuous )
let x, y be Element of L; :: according to WAYBEL_0:def 34 :: thesis: F preserves_inf_of {x,y}

assume ex_inf_of {x,y},L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of F .: {x,y}, BoolePoset H & "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) )

thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L))

A8: { f where f is Element of H : f . (x "/\" y) = 1 } c= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }

hence inf (F .: {x,y}) = (F . x) "/\" (F . y) by YELLOW_0:40

.= (F . x) /\ (F . y) by YELLOW_1:17

.= { f where f is Element of H : f . x = 1 } /\ (F . y) by A3

.= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A3

.= { f where f is Element of H : f . (x "/\" y) = 1 } by A18, A8

.= F . (x "/\" y) by A3

.= F . (inf {x,y}) by YELLOW_0:40 ;

:: thesis: verum

end;assume ex_inf_of {x,y},L ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of F .: {x,y}, BoolePoset H & "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) )

thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L))

A8: { f where f is Element of H : f . (x "/\" y) = 1 } c= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }

proof

A18:
{ f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "/\" y) = 1 }
A9:
( ex_inf_of {x,y},L & x "/\" y = inf {x,y} )
by YELLOW_0:17, YELLOW_0:40;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . (x "/\" y) = 1 } or p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } )

A10: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;

assume p in { f where f is Element of H : f . (x "/\" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }

then consider g being Element of H such that

A11: g = p and

A12: g . (x "/\" y) = 1 ;

g in H ;

then A13: ex a being Element of L st

( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;

then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;

g is meet-preserving by A13, Th33;

then A14: g preserves_inf_of {x,y} ;

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

then A15: {(g . x),(g . y)} = g .: {x,y} by FUNCT_1:60;

(g . x) "/\" (g . y) = inf {(g . x),(g . y)} by YELLOW_0:40;

then A16: g . (x "/\" y) = (g . x) "/\" (g . y) by A15, A14, A9;

then ( g . y <= Top (BoolePoset {{}}) & g . y >= Top (BoolePoset {{}}) ) by A12, A10, YELLOW_0:23, YELLOW_0:45;

then g . y = 1 by A10, ORDERS_2:2;

then A17: p in { f where f is Element of H : f . y = 1 } by A11;

( g . x <= Top (BoolePoset {{}}) & g . x >= Top (BoolePoset {{}}) ) by A12, A10, A16, YELLOW_0:23, YELLOW_0:45;

then g . x = 1 by A10, ORDERS_2:2;

then p in { f where f is Element of H : f . x = 1 } by A11;

hence p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A17, XBOOLE_0:def 4; :: thesis: verum

end;let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . (x "/\" y) = 1 } or p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } )

A10: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;

assume p in { f where f is Element of H : f . (x "/\" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }

then consider g being Element of H such that

A11: g = p and

A12: g . (x "/\" y) = 1 ;

g in H ;

then A13: ex a being Element of L st

( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;

then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;

g is meet-preserving by A13, Th33;

then A14: g preserves_inf_of {x,y} ;

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

then A15: {(g . x),(g . y)} = g .: {x,y} by FUNCT_1:60;

(g . x) "/\" (g . y) = inf {(g . x),(g . y)} by YELLOW_0:40;

then A16: g . (x "/\" y) = (g . x) "/\" (g . y) by A15, A14, A9;

then ( g . y <= Top (BoolePoset {{}}) & g . y >= Top (BoolePoset {{}}) ) by A12, A10, YELLOW_0:23, YELLOW_0:45;

then g . y = 1 by A10, ORDERS_2:2;

then A17: p in { f where f is Element of H : f . y = 1 } by A11;

( g . x <= Top (BoolePoset {{}}) & g . x >= Top (BoolePoset {{}}) ) by A12, A10, A16, YELLOW_0:23, YELLOW_0:45;

then g . x = 1 by A10, ORDERS_2:2;

then p in { f where f is Element of H : f . x = 1 } by A11;

hence p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A17, XBOOLE_0:def 4; :: thesis: verum

proof

F .: {x,y} = {(F . x),(F . y)}
by A2, FUNCT_1:60;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "/\" y) = 1 } )

A19: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40;

assume A20: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "/\" y) = 1 }

then p in { f where f is Element of H : f . x = 1 } by XBOOLE_0:def 4;

then consider f1 being Element of H such that

A21: f1 = p and

A22: f1 . x = 1 ;

p in { f where f is Element of H : f . y = 1 } by A20, XBOOLE_0:def 4;

then A23: ex f2 being Element of H st

( f2 = p & f2 . y = 1 ) ;

f1 in H ;

then consider a being Element of L such that

A24: chi (((downarrow a) `), the carrier of L) = f1 and

A25: a is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A24, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= a ) by A24, Th32;

then f1 is meet-preserving by A25, Th25;

then A26: f1 preserves_inf_of {x,y} ;

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

then A27: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

(f1 . x) "/\" (f1 . y) = inf {(f1 . x),(f1 . y)} by YELLOW_0:40;

then f1 . (x "/\" y) = (f1 . x) "/\" (f1 . y) by A27, A26, A19

.= 1 by A21, A22, A23, YELLOW_5:2 ;

hence p in { f where f is Element of H : f . (x "/\" y) = 1 } by A21; :: thesis: verum

end;A19: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0:40;

assume A20: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "/\" y) = 1 }

then p in { f where f is Element of H : f . x = 1 } by XBOOLE_0:def 4;

then consider f1 being Element of H such that

A21: f1 = p and

A22: f1 . x = 1 ;

p in { f where f is Element of H : f . y = 1 } by A20, XBOOLE_0:def 4;

then A23: ex f2 being Element of H st

( f2 = p & f2 . y = 1 ) ;

f1 in H ;

then consider a being Element of L such that

A24: chi (((downarrow a) `), the carrier of L) = f1 and

A25: a is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A24, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= a ) by A24, Th32;

then f1 is meet-preserving by A25, Th25;

then A26: f1 preserves_inf_of {x,y} ;

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

then A27: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

(f1 . x) "/\" (f1 . y) = inf {(f1 . x),(f1 . y)} by YELLOW_0:40;

then f1 . (x "/\" y) = (f1 . x) "/\" (f1 . y) by A27, A26, A19

.= 1 by A21, A22, A23, YELLOW_5:2 ;

hence p in { f where f is Element of H : f . (x "/\" y) = 1 } by A21; :: thesis: verum

hence inf (F .: {x,y}) = (F . x) "/\" (F . y) by YELLOW_0:40

.= (F . x) /\ (F . y) by YELLOW_1:17

.= { f where f is Element of H : f . x = 1 } /\ (F . y) by A3

.= { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A3

.= { f where f is Element of H : f . (x "/\" y) = 1 } by A18, A8

.= F . (x "/\" y) by A3

.= F . (inf {x,y}) by YELLOW_0:40 ;

:: thesis: verum

A29: F is V27()

proof

F is join-preserving
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )

assume that

A30: x1 in dom F and

A31: x2 in dom F and

A32: F . x1 = F . x2 ; :: thesis: x1 = x2

reconsider l2 = x2 as Element of L by A31;

reconsider l1 = x1 as Element of L by A30;

end;assume that

A30: x1 in dom F and

A31: x2 in dom F and

A32: F . x1 = F . x2 ; :: thesis: x1 = x2

reconsider l2 = x2 as Element of L by A31;

reconsider l1 = x1 as Element of L by A30;

now :: thesis: not l1 <> l2

hence
x1 = x2
; :: thesis: verumA33:
F . l2 = { f where f is Element of H : f . l2 = 1 }
by A3;

A34: F . l1 = { f where f is Element of H : f . l1 = 1 } by A3;

assume A35: l1 <> l2 ; :: thesis: contradiction

end;A34: F . l1 = { f where f is Element of H : f . l1 = 1 } by A3;

assume A35: l1 <> l2 ; :: thesis: contradiction

per cases
( not l1 <= l2 or not l2 <= l1 )
by A35, ORDERS_2:2;

end;

suppose
not l1 <= l2
; :: thesis: contradiction

then consider p being Element of L such that

A36: p in PRIME L and

A37: l2 <= p and

A38: not l1 <= p by A28, Th17;

set CH = chi (((downarrow p) `), the carrier of L);

p is prime by A36, Def7;

then chi (((downarrow p) `), the carrier of L) in H ;

then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;

then ( rng CH c= {0,1} & CH . l1 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;

then ( CH . l1 = 0 or CH . l1 = 1 ) by TARSKI:def 2;

hence contradiction by A32, A34, A38, A39, Th32; :: thesis: verum

end;A36: p in PRIME L and

A37: l2 <= p and

A38: not l1 <= p by A28, Th17;

set CH = chi (((downarrow p) `), the carrier of L);

p is prime by A36, Def7;

then chi (((downarrow p) `), the carrier of L) in H ;

then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;

A39: now :: thesis: not CH in F . l2

dom CH = the carrier of L
by FUNCT_2:def 1;assume
CH in F . l2
; :: thesis: contradiction

then ex f being Element of H st

( f = CH & f . l2 = 1 ) by A33;

hence contradiction by A37, Th32; :: thesis: verum

end;then ex f being Element of H st

( f = CH & f . l2 = 1 ) by A33;

hence contradiction by A37, Th32; :: thesis: verum

then ( rng CH c= {0,1} & CH . l1 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;

then ( CH . l1 = 0 or CH . l1 = 1 ) by TARSKI:def 2;

hence contradiction by A32, A34, A38, A39, Th32; :: thesis: verum

suppose
not l2 <= l1
; :: thesis: contradiction

then consider p being Element of L such that

A40: p in PRIME L and

A41: l1 <= p and

A42: not l2 <= p by A28, Th17;

set CH = chi (((downarrow p) `), the carrier of L);

p is prime by A40, Def7;

then chi (((downarrow p) `), the carrier of L) in H ;

then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;

then ( rng CH c= {0,1} & CH . l2 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;

then ( CH . l2 = 0 or CH . l2 = 1 ) by TARSKI:def 2;

hence contradiction by A32, A33, A42, A43, Th32; :: thesis: verum

end;A40: p in PRIME L and

A41: l1 <= p and

A42: not l2 <= p by A28, Th17;

set CH = chi (((downarrow p) `), the carrier of L);

p is prime by A40, Def7;

then chi (((downarrow p) `), the carrier of L) in H ;

then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;

A43: now :: thesis: not CH in F . l1

dom CH = the carrier of L
by FUNCT_2:def 1;assume
CH in F . l1
; :: thesis: contradiction

then ex f being Element of H st

( f = CH & f . l1 = 1 ) by A34;

hence contradiction by A41, Th32; :: thesis: verum

end;then ex f being Element of H st

( f = CH & f . l1 = 1 ) by A34;

hence contradiction by A41, Th32; :: thesis: verum

then ( rng CH c= {0,1} & CH . l2 in rng CH ) by FUNCT_1:def 3, RELAT_1:def 19;

then ( CH . l2 = 0 or CH . l2 = 1 ) by TARSKI:def 2;

hence contradiction by A32, A33, A42, A43, Th32; :: thesis: verum

proof

hence
L is distributive
by A7, A29, Th3; :: thesis: L is meet-continuous
let x, y be Element of L; :: according to WAYBEL_0:def 35 :: thesis: F preserves_sup_of {x,y}

assume ex_sup_of {x,y},L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: {x,y}, BoolePoset H & "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) )

thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L))

A44: { f where f is Element of H : f . (x "\/" y) = 1 } c= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }

hence sup (F .: {x,y}) = (F . x) "\/" (F . y) by YELLOW_0:41

.= (F . x) \/ (F . y) by YELLOW_1:17

.= { f where f is Element of H : f . x = 1 } \/ (F . y) by A3

.= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by A3

.= { f where f is Element of H : f . (x "\/" y) = 1 } by A56, A44

.= F . (x "\/" y) by A3

.= F . (sup {x,y}) by YELLOW_0:41 ;

:: thesis: verum

end;assume ex_sup_of {x,y},L ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: {x,y}, BoolePoset H & "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) )

thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L))

A44: { f where f is Element of H : f . (x "\/" y) = 1 } c= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }

proof

A56:
{ f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } c= { f where f is Element of H : f . (x "\/" y) = 1 }
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . (x "\/" y) = 1 } or p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } )

A45: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;

assume p in { f where f is Element of H : f . (x "\/" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }

then consider g being Element of H such that

A46: g = p and

A47: g . (x "\/" y) = 1 ;

g in H ;

then A48: ex a being Element of L st

( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;

then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;

g is join-preserving by A48, Th33;

then A49: g preserves_sup_of {x,y} ;

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

then A50: g .: {x,y} = {(g . x),(g . y)} by FUNCT_1:60;

A51: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

A52: (g . x) "\/" (g . y) = sup {(g . x),(g . y)} by YELLOW_0:41;

.= bool {{}} by YELLOW_1:1

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

then A55: ( g . y = {} or g . y = {{}} ) by TARSKI:def 2;

( g . x = {} or g . x = {{}} ) by A54, TARSKI:def 2;

then ( g . x = Top (BoolePoset {{}}) or g . y = Top (BoolePoset {{}}) ) by A55, A53, YELLOW_1:19;

then ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A46, A45;

hence p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by XBOOLE_0:def 3; :: thesis: verum

end;A45: 1 = Top (BoolePoset {{}}) by CARD_1:49, YELLOW_1:19;

assume p in { f where f is Element of H : f . (x "\/" y) = 1 } ; :: thesis: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }

then consider g being Element of H such that

A46: g = p and

A47: g . (x "\/" y) = 1 ;

g in H ;

then A48: ex a being Element of L st

( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;

then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;

g is join-preserving by A48, Th33;

then A49: g preserves_sup_of {x,y} ;

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

then A50: g .: {x,y} = {(g . x),(g . y)} by FUNCT_1:60;

A51: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

A52: (g . x) "\/" (g . y) = sup {(g . x),(g . y)} by YELLOW_0:41;

A53: now :: thesis: ( g . x = {} implies not g . y = {} )

A54: the carrier of (BoolePoset {{}}) =
the carrier of (InclPoset (bool {{}}))
by YELLOW_1:4
assume
( g . x = {} & g . y = {} )
; :: thesis: contradiction

then (g . x) "\/" (g . y) = {} \/ {} by YELLOW_1:17

.= 0 ;

hence contradiction by A47, A50, A49, A51, A52; :: thesis: verum

end;then (g . x) "\/" (g . y) = {} \/ {} by YELLOW_1:17

.= 0 ;

hence contradiction by A47, A50, A49, A51, A52; :: thesis: verum

.= bool {{}} by YELLOW_1:1

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

then A55: ( g . y = {} or g . y = {{}} ) by TARSKI:def 2;

( g . x = {} or g . x = {{}} ) by A54, TARSKI:def 2;

then ( g . x = Top (BoolePoset {{}}) or g . y = Top (BoolePoset {{}}) ) by A55, A53, YELLOW_1:19;

then ( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } ) by A46, A45;

hence p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by XBOOLE_0:def 3; :: thesis: verum

proof

F .: {x,y} = {(F . x),(F . y)}
by A2, FUNCT_1:60;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "\/" y) = 1 } )

assume A57: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }

end;assume A57: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }

per cases
( p in { f where f is Element of H : f . x = 1 } or p in { f where f is Element of H : f . y = 1 } )
by A57, XBOOLE_0:def 3;

end;

suppose
p in { f where f is Element of H : f . x = 1 }
; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }

then consider f1 being Element of H such that

A58: f1 = p and

A59: f1 . x = 1 ;

f1 in H ;

then consider a being Element of L such that

A60: chi (((downarrow a) `), the carrier of L) = f1 and

A61: a is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A60, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= a ) by A60, Th32;

then f1 is join-preserving by A61, Th25;

then A62: f1 preserves_sup_of {x,y} ;

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

then A63: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

A64: ( 1 = Top (BoolePoset {{}}) & f1 . y <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;

A65: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;

then f1 . (x "\/" y) = (f1 . x) "\/" (f1 . y) by A63, A62, A65

.= 1 by A59, A64, YELLOW_0:24 ;

hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A58; :: thesis: verum

end;A58: f1 = p and

A59: f1 . x = 1 ;

f1 in H ;

then consider a being Element of L such that

A60: chi (((downarrow a) `), the carrier of L) = f1 and

A61: a is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A60, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= a ) by A60, Th32;

then f1 is join-preserving by A61, Th25;

then A62: f1 preserves_sup_of {x,y} ;

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

then A63: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

A64: ( 1 = Top (BoolePoset {{}}) & f1 . y <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;

A65: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;

then f1 . (x "\/" y) = (f1 . x) "\/" (f1 . y) by A63, A62, A65

.= 1 by A59, A64, YELLOW_0:24 ;

hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A58; :: thesis: verum

suppose
p in { f where f is Element of H : f . y = 1 }
; :: thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }

then consider f1 being Element of H such that

A66: f1 = p and

A67: f1 . y = 1 ;

f1 in H ;

then consider b being Element of L such that

A68: chi (((downarrow b) `), the carrier of L) = f1 and

A69: b is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A68, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= b ) by A68, Th32;

then f1 is join-preserving by A69, Th25;

then A70: f1 preserves_sup_of {x,y} ;

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

then A71: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

A72: ( 1 = Top (BoolePoset {{}}) & f1 . x <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;

A73: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;

then f1 . (x "\/" y) = (f1 . y) "\/" (f1 . x) by A71, A70, A73

.= 1 by A67, A72, YELLOW_0:24 ;

hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A66; :: thesis: verum

end;A66: f1 = p and

A67: f1 . y = 1 ;

f1 in H ;

then consider b being Element of L such that

A68: chi (((downarrow b) `), the carrier of L) = f1 and

A69: b is prime ;

reconsider f1 = f1 as Function of L,(BoolePoset {{}}) by A68, Th31;

for x being Element of L holds

( f1 . x = {} iff x <= b ) by A68, Th32;

then f1 is join-preserving by A69, Th25;

then A70: f1 preserves_sup_of {x,y} ;

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

then A71: {(f1 . x),(f1 . y)} = f1 .: {x,y} by FUNCT_1:60;

A72: ( 1 = Top (BoolePoset {{}}) & f1 . x <= Top (BoolePoset {{}}) ) by CARD_1:49, YELLOW_0:45, YELLOW_1:19;

A73: ( ex_sup_of {x,y},L & x "\/" y = sup {x,y} ) by YELLOW_0:17, YELLOW_0:41;

(f1 . x) "\/" (f1 . y) = sup {(f1 . x),(f1 . y)} by YELLOW_0:41;

then f1 . (x "\/" y) = (f1 . y) "\/" (f1 . x) by A71, A70, A73

.= 1 by A67, A72, YELLOW_0:24 ;

hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A66; :: thesis: verum

hence sup (F .: {x,y}) = (F . x) "\/" (F . y) by YELLOW_0:41

.= (F . x) \/ (F . y) by YELLOW_1:17

.= { f where f is Element of H : f . x = 1 } \/ (F . y) by A3

.= { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by A3

.= { f where f is Element of H : f . (x "\/" y) = 1 } by A56, A44

.= F . (x "\/" y) by A3

.= F . (sup {x,y}) by YELLOW_0:41 ;

:: thesis: verum

F is sups-preserving

proof

hence
L is meet-continuous
by A7, A29, Th4; :: thesis: verum
let X be Subset of L; :: according to WAYBEL_0:def 33 :: thesis: F preserves_sup_of X

F preserves_sup_of X

end;F preserves_sup_of X

proof

hence
F preserves_sup_of X
; :: thesis: verum
assume
ex_sup_of X,L
; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of F .: X, BoolePoset H & "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) )

thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L))

A74: F . (sup X) = { g where g is Element of H : g . (sup X) = 1 } by A3;

A75: sup (F .: X) c= F . (sup X)

end;thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; :: thesis: "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L))

A74: F . (sup X) = { g where g is Element of H : g . (sup X) = 1 } by A3;

A75: sup (F .: X) c= F . (sup X)

proof

F . (sup X) c= sup (F .: X)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sup (F .: X) or a in F . (sup X) )

assume a in sup (F .: X) ; :: thesis: a in F . (sup X)

then a in union (F .: X) by YELLOW_1:21;

then consider Y being set such that

A76: a in Y and

A77: Y in F .: X by TARSKI:def 4;

consider z being object such that

A78: z in dom F and

A79: z in X and

A80: Y = F . z by A77, FUNCT_1:def 6;

reconsider z = z as Element of L by A78;

F . z = { f where f is Element of H : f . z = 1 } by A3;

then consider f being Element of H such that

A81: a = f and

A82: f . z = 1 by A76, A80;

f in H ;

then consider p being Element of L such that

A83: f = chi (((downarrow p) `), the carrier of L) and

p is prime ;

then A86: f . (sup X) in rng f by FUNCT_1:def 3;

rng f c= {0,1} by A83, RELAT_1:def 19;

then ( f . (sup X) = 0 or f . (sup X) = 1 ) by A86, TARSKI:def 2;

hence a in F . (sup X) by A74, A81, A84; :: thesis: verum

end;assume a in sup (F .: X) ; :: thesis: a in F . (sup X)

then a in union (F .: X) by YELLOW_1:21;

then consider Y being set such that

A76: a in Y and

A77: Y in F .: X by TARSKI:def 4;

consider z being object such that

A78: z in dom F and

A79: z in X and

A80: Y = F . z by A77, FUNCT_1:def 6;

reconsider z = z as Element of L by A78;

F . z = { f where f is Element of H : f . z = 1 } by A3;

then consider f being Element of H such that

A81: a = f and

A82: f . z = 1 by A76, A80;

f in H ;

then consider p being Element of L such that

A83: f = chi (((downarrow p) `), the carrier of L) and

p is prime ;

A84: now :: thesis: not f . (sup X) = 0

dom f = the carrier of L
by A83, FUNCT_2:def 1;
sup X is_>=_than X
by YELLOW_0:32;

then A85: z <= sup X by A79;

assume f . (sup X) = 0 ; :: thesis: contradiction

then sup X <= p by A83, Th32;

then z <= p by A85, ORDERS_2:3;

hence contradiction by A82, A83, Th32; :: thesis: verum

end;then A85: z <= sup X by A79;

assume f . (sup X) = 0 ; :: thesis: contradiction

then sup X <= p by A83, Th32;

then z <= p by A85, ORDERS_2:3;

hence contradiction by A82, A83, Th32; :: thesis: verum

then A86: f . (sup X) in rng f by FUNCT_1:def 3;

rng f c= {0,1} by A83, RELAT_1:def 19;

then ( f . (sup X) = 0 or f . (sup X) = 1 ) by A86, TARSKI:def 2;

hence a in F . (sup X) by A74, A81, A84; :: thesis: verum

proof

hence
"\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L))
by A75; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in F . (sup X) or a in sup (F .: X) )

assume a in F . (sup X) ; :: thesis: a in sup (F .: X)

then consider f being Element of H such that

A87: a = f and

A88: f . (sup X) = 1 by A74;

f in H ;

then consider p being Element of L such that

A89: f = chi (((downarrow p) `), the carrier of L) and

p is prime ;

A90: rng f c= {0,1} by A89, RELAT_1:def 19;

A91: not sup X <= p by A88, A89, Th32;

A92: l in X and

A93: not l <= p ;

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

then f . l in rng f by FUNCT_1:def 3;

then ( f . l = 0 or f . l = 1 ) by A90, TARSKI:def 2;

then f in { g where g is Element of H : g . l = 1 } by A89, A93, Th32;

then A94: f in F . l by A3;

F . l in F .: X by A2, A92, FUNCT_1:def 6;

then a in union (F .: X) by A87, A94, TARSKI:def 4;

hence a in sup (F .: X) by YELLOW_1:21; :: thesis: verum

end;assume a in F . (sup X) ; :: thesis: a in sup (F .: X)

then consider f being Element of H such that

A87: a = f and

A88: f . (sup X) = 1 by A74;

f in H ;

then consider p being Element of L such that

A89: f = chi (((downarrow p) `), the carrier of L) and

p is prime ;

A90: rng f c= {0,1} by A89, RELAT_1:def 19;

A91: not sup X <= p by A88, A89, Th32;

now :: thesis: ex l being Element of L st

( l in X & not l <= p )

then consider l being Element of L such that ( l in X & not l <= p )

assume
for l being Element of L st l in X holds

l <= p ; :: thesis: contradiction

then X is_<=_than p ;

hence contradiction by A91, YELLOW_0:32; :: thesis: verum

end;l <= p ; :: thesis: contradiction

then X is_<=_than p ;

hence contradiction by A91, YELLOW_0:32; :: thesis: verum

A92: l in X and

A93: not l <= p ;

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

then f . l in rng f by FUNCT_1:def 3;

then ( f . l = 0 or f . l = 1 ) by A90, TARSKI:def 2;

then f in { g where g is Element of H : g . l = 1 } by A89, A93, Th32;

then A94: f in F . l by A3;

F . l in F .: X by A2, A92, FUNCT_1:def 6;

then a in union (F .: X) by A87, A94, TARSKI:def 4;

hence a in sup (F .: X) by YELLOW_1:21; :: thesis: verum