let T be TopSpace; :: thesis: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice
set L = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #);
A1: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-commutative
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 4 :: thesis: a "\/" b = b "\/" a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
thus a "\/" b = B \/ A by Def6
.= b "\/" a by Def6 ; :: thesis: verum
end;
A2: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-absorbing
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 8 :: thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Closed_Domains_of T ;
A3: (Cl (Int A)) /\ B c= B by XBOOLE_1:17;
B in { D where D is Subset of T : D is closed_condensed } ;
then ex D being Subset of T st
( D = B & D is closed_condensed ) ;
then A4: B = Cl (Int B) by TOPS_1:def 7;
Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:17;
then A5: Cl (Int (A /\ B)) c= (Cl (Int A)) /\ B by A4, PRE_TOPC:21;
a "/\" b = Cl (Int (A /\ B)) by Def7;
hence (a "/\" b) "\/" b = (Cl (Int (A /\ B))) \/ B by Def6
.= b by A5, A3, XBOOLE_1:1, XBOOLE_1:12 ;
:: thesis: verum
end;
A6: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-absorbing
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 9 :: thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then A7: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
a "\/" b = A \/ B by Def6;
hence a "/\" (a "\/" b) = Cl (Int (A /\ (A \/ B))) by Def7
.= Cl (Int A) by XBOOLE_1:21
.= a by A7, TOPS_1:def 7 ;
:: thesis: verum
end;
A8: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is join-associative
proof
let a, b, c be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 5 :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A9: a "\/" b = A \/ B by Def6;
b "\/" c = B \/ C by Def6;
hence a "\/" (b "\/" c) = A \/ (B \/ C) by Def6
.= (A \/ B) \/ C by XBOOLE_1:4
.= (a "\/" b) "\/" c by A9, Def6 ;
:: thesis: verum
end;
A10: LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-associative
proof
let a, b, c be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 7 :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then A11: ex D being Subset of T st
( D = A & D is closed_condensed ) ;
B in { E where E is Subset of T : E is closed_condensed } ;
then A12: ex E being Subset of T st
( E = B & E is closed_condensed ) ;
C in { F where F is Subset of T : F is closed_condensed } ;
then A13: ex F being Subset of T st
( F = C & F is closed_condensed ) ;
A14: a "/\" b = Cl (Int (A /\ B)) by Def7;
b "/\" c = Cl (Int (B /\ C)) by Def7;
hence a "/\" (b "/\" c) = Cl (Int (A /\ (Cl (Int (B /\ C))))) by Def7
.= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A11, A12, A13, Th28
.= (a "/\" b) "/\" c by A14, Def7 ;
:: thesis: verum
end;
LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is meet-commutative
proof
let a, b be Element of LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #); :: according to LATTICES:def 6 :: thesis: a "/\" b = b "/\" a
reconsider A = a, B = b as Element of Closed_Domains_of T ;
thus a "/\" b = Cl (Int (B /\ A)) by Def7
.= b "/\" a by Def7 ; :: thesis: verum
end;
then reconsider L = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) as Lattice by A1, A8, A2, A10, A6;
A15: L is upper-bounded
proof
[#] T is closed_condensed by Th19;
then [#] T in { D where D is Subset of T : D is closed_condensed } ;
then reconsider c = [#] T as Element of L ;
take c ; :: according to LATTICES:def 14 :: thesis: for b1 being Element of the carrier of L holds
( c "\/" b1 = c & b1 "\/" c = c )
let a be Element of L; :: thesis: ( c "\/" a = c & a "\/" c = c )
reconsider C = c, A = a as Element of Closed_Domains_of T ;
thus c "\/" a = C \/ A by Def6
.= c by XBOOLE_1:12 ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum
end;
A16: L is distributive
proof
let a, b, c be Element of L; :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider A = a, B = b, C = c as Element of Closed_Domains_of T ;
A in { D where D is Subset of T : D is closed_condensed } ;
then consider D being Subset of T such that
A17: D = A and
A18: D is closed_condensed ;
A19: D is closed by A18, TOPS_1:66;
B in { E where E is Subset of T : E is closed_condensed } ;
then consider E being Subset of T such that
A20: E = B and
A21: E is closed_condensed ;
A22: E is closed by A21, TOPS_1:66;
A23: a "/\" c = Cl (Int (A /\ C)) by Def7;
A24: a "/\" b = Cl (Int (A /\ B)) by Def7;
b "\/" c = B \/ C by Def6;
hence a "/\" (b "\/" c) = Cl (Int (A /\ (B \/ C))) by Def7
.= Cl (Int ((A /\ B) \/ (A /\ C))) by XBOOLE_1:23
.= (Cl (Int (A /\ B))) \/ (Cl (Int (A /\ C))) by A17, A20, A19, A22, Th6
.= (a "/\" b) "\/" (a "/\" c) by A24, A23, Def6 ;
:: thesis: verum
end;
A25: L is complemented
proof
[#] T is closed_condensed by Th19;
then [#] T in { K where K is Subset of T : K is closed_condensed } ;
then reconsider c = [#] T as Element of L ;
let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of b
reconsider B = b as Element of Closed_Domains_of T ;
B in { D where D is Subset of T : D is closed_condensed } ;
then consider D being Subset of T such that
A26: D = B and
A27: D is closed_condensed ;
D is condensed by A27, TOPS_1:66;
then Cl (B `) is closed_condensed by A26, Th16, Th24;
then Cl (B `) in { K where K is Subset of T : K is closed_condensed } ;
then reconsider a = Cl (B `) as Element of L ;
take a ; :: thesis: a is_a_complement_of b
A28: D is closed by A27, TOPS_1:66;
A29: for v being Element of L holds the L_meet of L . (c,v) = v
proof
let v be Element of L; :: thesis: the L_meet of L . (c,v) = v
reconsider V = v as Element of Closed_Domains_of T ;
V in { K where K is Subset of T : K is closed_condensed } ;
then A30: ex D being Subset of T st
( D = V & D is closed_condensed ) ;
thus the L_meet of L . (c,v) = Cl (Int (([#] T) /\ V)) by Def7
.= Cl (Int V) by XBOOLE_1:28
.= v by A30, TOPS_1:def 7 ; :: thesis: verum
end;
thus a "\/" b = (Cl (B `)) \/ B by Def6
.= (Cl (D `)) \/ (Cl D) by A26, A28, PRE_TOPC:22
.= Cl ((B `) \/ B) by A26, PRE_TOPC:20
.= Cl ([#] T) by PRE_TOPC:2
.= c by TOPS_1:2
.= Top L by A29, LATTICE2:17 ; :: according to LATTICES:def 18 :: thesis: ( b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L )
hence b "\/" a = Top L ; :: thesis: ( a "/\" b = Bottom L & b "/\" a = Bottom L )
{} T is closed_condensed by Th18;
then {} T in { K where K is Subset of T : K is closed_condensed } ;
then reconsider c = {} T as Element of L ;
A31: for v being Element of L holds the L_join of L . (c,v) = v
proof
let v be Element of L; :: thesis: the L_join of L . (c,v) = v
reconsider V = v as Element of Closed_Domains_of T ;
thus the L_join of L . (c,v) = ({} T) \/ V by Def6
.= (([#] T) `) \/ ((V `) `) by XBOOLE_1:37
.= (([#] T) /\ (V `)) ` by XBOOLE_1:54
.= (V `) ` by XBOOLE_1:28
.= v ; :: thesis: verum
end;
thus a "/\" b = Cl (Int (B /\ (Cl (B `)))) by Def7
.= Cl ({} T) by Th8
.= c by PRE_TOPC:22
.= Bottom L by A31, LATTICE2:15 ; :: thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; :: thesis: verum
end;
L is lower-bounded
proof
A32: {} T is closed_condensed by Th18;
then {} T in { D where D is Subset of T : D is closed_condensed } ;
then reconsider c = {} T as Element of L ;
take c ; :: according to LATTICES:def 13 :: thesis: for b1 being Element of the carrier of L holds
( c "/\" b1 = c & b1 "/\" c = c )
let a be Element of L; :: thesis: ( c "/\" a = c & a "/\" c = c )
reconsider C = c, A = a as Element of Closed_Domains_of T ;
thus c "/\" a = Cl (Int (C /\ A)) by Def7
.= c by A32, TOPS_1:def 7 ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum
end;
hence LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice by A15, A25, A16; :: thesis: verum