let BL be Boolean Lattice; :: thesis: for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds

for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

let AF be non empty ClosedSubset of BL; :: thesis: ( Bottom BL in AF & Top BL in AF implies for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )

assume that

A1: Bottom BL in AF and

A2: Top BL in AF ; :: thesis: for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

set C = { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ;

A3: { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF_{1}[ Element of Fin the carrier of BL] means ( $1 c= SetImp AF implies ex B0 being Element of Fin the carrier of BL st

( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ($1,(comp BL)) = FinMeet B0 ) );

let B be Element of Fin the carrier of BL; :: thesis: ( B c= SetImp AF implies ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )

assume A8: B c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

A9: for B9 being Element of Fin the carrier of BL

for b being Element of BL st S_{1}[B9] holds

S_{1}[B9 \/ {.b.}]
_{1}[ {}. the carrier of BL]
_{1}[B]
from SETWISEO:sch 4(A31, A9);

then ex B1 being Element of Fin the carrier of BL st

( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B,(comp BL)) = FinMeet B1 ) by A8;

hence ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) by A3, XBOOLE_1:1; :: thesis: verum

for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

let AF be non empty ClosedSubset of BL; :: thesis: ( Bottom BL in AF & Top BL in AF implies for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )

assume that

A1: Bottom BL in AF and

A2: Top BL in AF ; :: thesis: for B being Element of Fin the carrier of BL st B c= SetImp AF holds

ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

set C = { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ;

A3: { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } c= SetImp AF

proof

defpred S
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } or x in SetImp AF )

assume x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: x in SetImp AF

then consider A1, A2 being Element of Fin the carrier of BL such that

A4: x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A5: ( A1 c= AF & A2 c= AF ) ;

consider p, q being Element of BL such that

A6: ( p = FinMeet A2 & q = FinJoin A1 ) ;

A7: x = (p `) "\/" q by A4, A6, Th41;

( p in AF & q in AF ) by A1, A2, A5, A6, Th17, Th24;

hence x in SetImp AF by A7, Th37; :: thesis: verum

end;assume x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } ; :: thesis: x in SetImp AF

then consider A1, A2 being Element of Fin the carrier of BL such that

A4: x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A5: ( A1 c= AF & A2 c= AF ) ;

consider p, q being Element of BL such that

A6: ( p = FinMeet A2 & q = FinJoin A1 ) ;

A7: x = (p `) "\/" q by A4, A6, Th41;

( p in AF & q in AF ) by A1, A2, A5, A6, Th17, Th24;

hence x in SetImp AF by A7, Th37; :: thesis: verum

( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ($1,(comp BL)) = FinMeet B0 ) );

let B be Element of Fin the carrier of BL; :: thesis: ( B c= SetImp AF implies ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) )

assume A8: B c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )

A9: for B9 being Element of Fin the carrier of BL

for b being Element of BL st S

S

proof

A31:
S
set J = the L_join of BL;

let B9 be Element of Fin the carrier of BL; :: thesis: for b being Element of BL st S_{1}[B9] holds

S_{1}[B9 \/ {.b.}]

let b be Element of BL; :: thesis: ( S_{1}[B9] implies S_{1}[B9 \/ {.b.}] )

assume A10: ( B9 c= SetImp AF implies ex B1 being Element of Fin the carrier of BL st

( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B9,(comp BL)) = FinMeet B1 ) ) ; :: thesis: S_{1}[B9 \/ {.b.}]

assume A11: B9 \/ {b} c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st

( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet B0 )

then consider B1 being Element of Fin the carrier of BL such that

A12: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } and

A13: FinJoin (B9,(comp BL)) = FinMeet B1 by A10, ZFMISC_1:137;

b in SetImp AF by A11, ZFMISC_1:137;

then consider p, q being Element of BL such that

A14: b = (p `) "\/" q and

A15: p in AF and

A16: q in AF by Th37;

A17: for x being set

for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds

ex a being Element of BL st

( a in B1 & x = a "\/" b )

b ` = ((p `) `) "/\" (q `) by A14, LATTICES:24

.= p "/\" (q `) ;

then FinJoin ((B9 \/ {.b.}),(comp BL)) = (FinMeet B1) "\/" (p "/\" (q `)) by A13, Th38

.= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q `)) by LATTICES:11

.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" ((FinMeet B1) "\/" (q `)) by Th25

.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" (FinMeet (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th25

.= FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th23 ;

hence ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) by A21, A26, XBOOLE_1:8; :: thesis: verum

end;let B9 be Element of Fin the carrier of BL; :: thesis: for b being Element of BL st S

S

let b be Element of BL; :: thesis: ( S

assume A10: ( B9 c= SetImp AF implies ex B1 being Element of Fin the carrier of BL st

( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B9,(comp BL)) = FinMeet B1 ) ) ; :: thesis: S

assume A11: B9 \/ {b} c= SetImp AF ; :: thesis: ex B0 being Element of Fin the carrier of BL st

( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet B0 )

then consider B1 being Element of Fin the carrier of BL such that

A12: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } and

A13: FinJoin (B9,(comp BL)) = FinMeet B1 by A10, ZFMISC_1:137;

b in SetImp AF by A11, ZFMISC_1:137;

then consider p, q being Element of BL such that

A14: b = (p `) "\/" q and

A15: p in AF and

A16: q in AF by Th37;

A17: for x being set

for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds

ex a being Element of BL st

( a in B1 & x = a "\/" b )

proof

A21:
( the L_join of BL [:] ((id BL),p)) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
let x be set ; :: thesis: for b being Element of BL st x in ( the L_join of BL [:] ((id BL),b)) .: B1 holds

ex a being Element of BL st

( a in B1 & x = a "\/" b )

let b be Element of BL; :: thesis: ( x in ( the L_join of BL [:] ((id BL),b)) .: B1 implies ex a being Element of BL st

( a in B1 & x = a "\/" b ) )

assume A18: x in ( the L_join of BL [:] ((id BL),b)) .: B1 ; :: thesis: ex a being Element of BL st

( a in B1 & x = a "\/" b )

( the L_join of BL [:] ((id BL),b)) .: B1 c= the carrier of BL by FUNCT_2:36;

then reconsider x = x as Element of BL by A18;

consider a being Element of BL such that

A19: a in B1 and

A20: x = ( the L_join of BL [:] ((id BL),b)) . a by A18, FUNCT_2:65;

x = the L_join of BL . (((id BL) . a),b) by A20, FUNCOP_1:48

.= a "\/" b by FUNCT_1:18 ;

hence ex a being Element of BL st

( a in B1 & x = a "\/" b ) by A19; :: thesis: verum

end;ex a being Element of BL st

( a in B1 & x = a "\/" b )

let b be Element of BL; :: thesis: ( x in ( the L_join of BL [:] ((id BL),b)) .: B1 implies ex a being Element of BL st

( a in B1 & x = a "\/" b ) )

assume A18: x in ( the L_join of BL [:] ((id BL),b)) .: B1 ; :: thesis: ex a being Element of BL st

( a in B1 & x = a "\/" b )

( the L_join of BL [:] ((id BL),b)) .: B1 c= the carrier of BL by FUNCT_2:36;

then reconsider x = x as Element of BL by A18;

consider a being Element of BL such that

A19: a in B1 and

A20: x = ( the L_join of BL [:] ((id BL),b)) . a by A18, FUNCT_2:65;

x = the L_join of BL . (((id BL) . a),b) by A20, FUNCOP_1:48

.= a "\/" b by FUNCT_1:18 ;

hence ex a being Element of BL st

( a in B1 & x = a "\/" b ) by A19; :: thesis: verum

proof

A26:
( the L_join of BL [:] ((id BL),(q `))) .: B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( the L_join of BL [:] ((id BL),p)) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )

assume x in ( the L_join of BL [:] ((id BL),p)) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then consider a being Element of BL such that

A22: a in B1 and

A23: x = a "\/" p by A17;

a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A22;

then consider A1, A2 being Element of Fin the carrier of BL such that

A24: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A25: ( A1 c= AF & A2 c= AF ) ;

ex A19, A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

end;assume x in ( the L_join of BL [:] ((id BL),p)) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then consider a being Element of BL such that

A22: a in B1 and

A23: x = a "\/" p by A17;

a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A22;

then consider A1, A2 being Element of Fin the carrier of BL such that

A24: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A25: ( A1 c= AF & A2 c= AF ) ;

ex A19, A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

proof

hence
x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
; :: thesis: verum
take A19 = A1 \/ {.p.}; :: thesis: ex A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

take A29 = A2; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

x = ((FinJoin A1) "\/" p) "\/" (FinJoin (A2,(comp BL))) by A23, A24, LATTICES:def 5

.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th14 ;

hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A15, A25, ZFMISC_1:137; :: thesis: verum

end;( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

take A29 = A2; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

x = ((FinJoin A1) "\/" p) "\/" (FinJoin (A2,(comp BL))) by A23, A24, LATTICES:def 5

.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th14 ;

hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A15, A25, ZFMISC_1:137; :: thesis: verum

proof

take
(( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)
; :: thesis: ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )

assume x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then consider a being Element of BL such that

A27: a in B1 and

A28: x = a "\/" (q `) by A17;

a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A27;

then consider A1, A2 being Element of Fin the carrier of BL such that

A29: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A30: ( A1 c= AF & A2 c= AF ) ;

ex A19, A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

end;assume x in ( the L_join of BL [:] ((id BL),(q `))) .: B1 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then consider a being Element of BL such that

A27: a in B1 and

A28: x = a "\/" (q `) by A17;

a in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } by A12, A27;

then consider A1, A2 being Element of Fin the carrier of BL such that

A29: a = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) and

A30: ( A1 c= AF & A2 c= AF ) ;

ex A19, A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

proof

hence
x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
; :: thesis: verum
take A19 = A1; :: thesis: ex A29 being Element of Fin the carrier of BL st

( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

take A29 = A2 \/ {.q.}; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

x = (FinJoin A1) "\/" ((FinJoin (A2,(comp BL))) "\/" (q `)) by A28, A29, LATTICES:def 5

.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th38 ;

hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A16, A30, ZFMISC_1:137; :: thesis: verum

end;( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

take A29 = A2 \/ {.q.}; :: thesis: ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF )

x = (FinJoin A1) "\/" ((FinJoin (A2,(comp BL))) "\/" (q `)) by A28, A29, LATTICES:def 5

.= (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) by Th38 ;

hence ( x = (FinJoin A19) "\/" (FinJoin (A29,(comp BL))) & A19 c= AF & A29 c= AF ) by A16, A30, ZFMISC_1:137; :: thesis: verum

b ` = ((p `) `) "/\" (q `) by A14, LATTICES:24

.= p "/\" (q `) ;

then FinJoin ((B9 \/ {.b.}),(comp BL)) = (FinMeet B1) "\/" (p "/\" (q `)) by A13, Th38

.= ((FinMeet B1) "\/" p) "/\" ((FinMeet B1) "\/" (q `)) by LATTICES:11

.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" ((FinMeet B1) "\/" (q `)) by Th25

.= (FinMeet (( the L_join of BL [:] ((id BL),p)) .: B1)) "/\" (FinMeet (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th25

.= FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) by Th23 ;

hence ( (( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1) c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin ((B9 \/ {.b.}),(comp BL)) = FinMeet ((( the L_join of BL [:] ((id BL),p)) .: B1) \/ (( the L_join of BL [:] ((id BL),(q `))) .: B1)) ) by A21, A26, XBOOLE_1:8; :: thesis: verum

proof

for B being Element of Fin the carrier of BL holds S
assume
{}. the carrier of BL c= SetImp AF
; :: thesis: ex B0 being Element of Fin the carrier of BL st

( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )

take B0 = {.(Bottom BL).}; :: thesis: ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )

A32: B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

.= FinMeet {.(Bottom BL).} by Th10 ;

hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) by A32; :: thesis: verum

end;( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )

take B0 = {.(Bottom BL).}; :: thesis: ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 )

A32: B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

proof

FinJoin (({}. the carrier of BL),(comp BL)) =
Bottom BL
by Lm1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B0 or x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } )

assume x in B0 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then A33: x = Bottom BL by TARSKI:def 1;

ex A1, A2 being Element of Fin the carrier of BL st

( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

end;assume x in B0 ; :: thesis: x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }

then A33: x = Bottom BL by TARSKI:def 1;

ex A1, A2 being Element of Fin the carrier of BL st

( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

proof

hence
x in { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) }
; :: thesis: verum
take A1 = {.(Bottom BL).}; :: thesis: ex A2 being Element of Fin the carrier of BL st

( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

take A2 = {.(Top BL).}; :: thesis: ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

thus x = (Bottom BL) "\/" (Bottom BL) by A33

.= (Bottom BL) "\/" ((Top BL) `) by Th29

.= (FinJoin A1) "\/" ((Top BL) `) by Th9

.= (FinJoin A1) "\/" ((FinMeet A2) `) by Th10

.= (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) by Th41 ; :: thesis: ( A1 c= AF & A2 c= AF )

thus A1 c= AF by A1, ZFMISC_1:31; :: thesis: A2 c= AF

thus A2 c= AF by A2, ZFMISC_1:31; :: thesis: verum

end;( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

take A2 = {.(Top BL).}; :: thesis: ( x = (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) & A1 c= AF & A2 c= AF )

thus x = (Bottom BL) "\/" (Bottom BL) by A33

.= (Bottom BL) "\/" ((Top BL) `) by Th29

.= (FinJoin A1) "\/" ((Top BL) `) by Th9

.= (FinJoin A1) "\/" ((FinMeet A2) `) by Th10

.= (FinJoin A1) "\/" (FinJoin (A2,(comp BL))) by Th41 ; :: thesis: ( A1 c= AF & A2 c= AF )

thus A1 c= AF by A1, ZFMISC_1:31; :: thesis: A2 c= AF

thus A2 c= AF by A2, ZFMISC_1:31; :: thesis: verum

.= FinMeet {.(Bottom BL).} by Th10 ;

hence ( B0 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (({}. the carrier of BL),(comp BL)) = FinMeet B0 ) by A32; :: thesis: verum

then ex B1 being Element of Fin the carrier of BL st

( B1 c= { ((FinJoin A1) "\/" (FinJoin (A2,(comp BL)))) where A1, A2 is Element of Fin the carrier of BL : ( A1 c= AF & A2 c= AF ) } & FinJoin (B,(comp BL)) = FinMeet B1 ) by A8;

hence ex B0 being Element of Fin the carrier of BL st

( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 ) by A3, XBOOLE_1:1; :: thesis: verum