let T be TopSpace; :: thesis: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice
set L = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #);
LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is Lattice-like
proof
thus for a, b being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds a "\/" b = b "\/" a :: according to LATTICES:def 4,LATTICES:def 10 :: thesis: ( LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-associative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-absorbing & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-commutative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: a "\/" b = b "\/" a
reconsider A = a, B = b as Element of Open_Domains_of T ;
thus a "\/" b = Int (Cl (B \/ A)) by Def10
.= b "\/" a by Def10 ; :: thesis: verum
end;
thus for a, b, c being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c :: according to LATTICES:def 5 :: thesis: ( LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-absorbing & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-commutative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing )
proof
let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider A = a, B = b, C = c as Element of Open_Domains_of T ;
( A in { D where D is Subset of T : D is open_condensed } & B in { E where E is Subset of T : E is open_condensed } & C in { F where F is Subset of T : F is open_condensed } ) ;
then A1: ( ex D being Subset of T st
( D = A & D is open_condensed ) & ex E being Subset of T st
( E = B & E is open_condensed ) & ex F being Subset of T st
( F = C & F is open_condensed ) ) ;
A2: b "\/" c = Int (Cl (B \/ C)) by Def10;
A3: a "\/" b = Int (Cl (A \/ B)) by Def10;
thus a "\/" (b "\/" c) = Int (Cl (A \/ (Int (Cl (B \/ C))))) by A2, Def10
.= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A1, Th29
.= (a "\/" b) "\/" c by A3, Def10 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds (a "/\" b) "\/" b = b :: according to LATTICES:def 8 :: thesis: ( LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-commutative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: (a "/\" b) "\/" b = b
reconsider A = a, B = b as Element of Open_Domains_of T ;
A4: a "/\" b = A /\ B by Def11;
B in { D where D is Subset of T : D is open_condensed } ;
then A5: ex D being Subset of T st
( D = B & D is open_condensed ) ;
thus (a "/\" b) "\/" b = Int (Cl ((A /\ B) \/ B)) by A4, Def10
.= Int (Cl B) by XBOOLE_1:22
.= b by A5, TOPS_1:def 8 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds a "/\" b = b "/\" a :: according to LATTICES:def 6 :: thesis: ( LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative & LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing )
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: a "/\" b = b "/\" a
reconsider A = a, B = b as Element of Open_Domains_of T ;
thus a "/\" b = B /\ A by Def11
.= b "/\" a by Def11 ; :: thesis: verum
end;
thus for a, b, c being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c :: according to LATTICES:def 7 :: thesis: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-absorbing
proof
let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider A = a, B = b, C = c as Element of Open_Domains_of T ;
A6: b "/\" c = B /\ C by Def11;
A7: a "/\" b = A /\ B by Def11;
thus a "/\" (b "/\" c) = A /\ (B /\ C) by A6, Def11
.= (A /\ B) /\ C by XBOOLE_1:16
.= (a "/\" b) "/\" c by A7, Def11 ; :: thesis: verum
end;
thus for a, b being Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) holds a "/\" (a "\/" b) = a :: according to LATTICES:def 9 :: thesis: verum
proof
let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: thesis: a "/\" (a "\/" b) = a
reconsider A = a, B = b as Element of Open_Domains_of T ;
A8: a "\/" b = Int (Cl (A \/ B)) by Def10;
A in { D where D is Subset of T : D is open_condensed } ;
then ex D being Subset of T st
( D = A & D is open_condensed ) ;
then A9: A = Int (Cl A) by TOPS_1:def 8;
Int ((Cl A) \/ (Cl B)) = Int (Cl (A \/ B)) by PRE_TOPC:50;
then A10: ( A c= A \/ (Int (Cl B)) & A \/ (Int (Cl B)) c= Int (Cl (A \/ B)) ) by A9, TOPS_1:49, XBOOLE_1:7;
thus a "/\" (a "\/" b) = A /\ (Int (Cl (A \/ B))) by A8, Def11
.= a by A10, XBOOLE_1:1, XBOOLE_1:28 ; :: thesis: verum
end;
end;
then reconsider L = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) as Lattice ;
L is Boolean
proof
thus L is lower-bounded :: according to LATTICES:def 15,LATTICES:def 20 :: thesis: ( L is upper-bounded & L is complemented & L is distributive )
proof
{} T is open_condensed by Th20;
then {} T in { D where D is Subset of T : D is open_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 Open_Domains_of T ;
thus c "/\" a = C /\ A by Def11
.= c ; :: thesis: a "/\" c = c
hence a "/\" c = c ; :: thesis: verum
end;
thus L is upper-bounded :: thesis: ( L is complemented & L is distributive )
proof
A11: [#] T is open_condensed by Th21;
then [#] T in { D where D is Subset of T : D is open_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 Open_Domains_of T ;
thus c "\/" a = Int (Cl (C \/ A)) by Def10
.= Int (Cl C) by XBOOLE_1:12
.= c by A11, TOPS_1:def 8 ; :: thesis: a "\/" c = c
hence a "\/" c = c ; :: thesis: verum
end;
thus L is complemented :: thesis: L is distributive
proof
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 Open_Domains_of T ;
B in { D where D is Subset of T : D is open_condensed } ;
then consider D being Subset of T such that
A12: ( D = B & D is open_condensed ) ;
A13: ( D is condensed & D is open ) by A12, TOPS_1:107;
then Int (B ` ) is open_condensed by A12, Th16, Th25;
then Int (B ` ) in { K where K is Subset of T : K is open_condensed } ;
then reconsider a = Int (B ` ) as Element of L ;
take a ; :: thesis: a is_a_complement_of b
[#] T is open_condensed by Th21;
then [#] T in { K where K is Subset of T : K is open_condensed } ;
then reconsider c = [#] T as Element of L ;
A14: 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 Open_Domains_of T ;
thus the L_meet of L . c,v = ([#] T) /\ V by Def11
.= v by XBOOLE_1:28 ; :: thesis: verum
end;
thus a "\/" b = Int (Cl (B \/ (Int (B ` )))) by Def10
.= Int ([#] T) by Th9
.= c by TOPS_1:43
.= Top L by A14, LATTICE2:25 ; :: 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 open_condensed by Th20;
then {} T in { K where K is Subset of T : K is open_condensed } ;
then reconsider c = {} T as Element of L ;
A15: 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 Open_Domains_of T ;
V in { K where K is Subset of T : K is open_condensed } ;
then A16: ex D being Subset of T st
( D = V & D is open_condensed ) ;
thus the L_join of L . c,v = Int (Cl (({} T) \/ V)) by Def10
.= Int (Cl ((([#] T) ` ) \/ ((V ` ) ` ))) by XBOOLE_1:37
.= Int (Cl ((([#] T) /\ (V ` )) ` )) by XBOOLE_1:54
.= Int (Cl ((V ` ) ` )) by XBOOLE_1:28
.= v by A16, TOPS_1:def 8 ; :: thesis: verum
end;
A17: B ` misses B by XBOOLE_1:79;
thus a "/\" b = (Int (B ` )) /\ B by Def11
.= (Int (D ` )) /\ (Int D) by A12, A13, TOPS_1:55
.= Int ((B ` ) /\ B) by A12, TOPS_1:46
.= Int ({} T) by A17, XBOOLE_0:def 7
.= Bottom L by A15, LATTICE2:22 ; :: thesis: b "/\" a = Bottom L
hence b "/\" a = Bottom L ; :: thesis: verum
end;
thus L is distributive :: thesis: verum
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 Open_Domains_of T ;
A18: ( A in { D where D is Subset of T : D is open_condensed } & B in { E where E is Subset of T : E is open_condensed } & C in { F where F is Subset of T : F is open_condensed } ) ;
then consider D being Subset of T such that
A19: ( D = A & D is open_condensed ) ;
consider E being Subset of T such that
A20: ( E = B & E is open_condensed ) by A18;
consider F being Subset of T such that
A21: ( F = C & F is open_condensed ) by A18;
A22: ( D is open & E is open & F is open ) by A19, A20, A21, TOPS_1:107;
A23: b "\/" c = Int (Cl (B \/ C)) by Def10;
A24: a "/\" b = A /\ B by Def11;
A25: a "/\" c = A /\ C by Def11;
thus a "/\" (b "\/" c) = A /\ (Int (Cl (B \/ C))) by A23, Def11
.= (Int (Cl A)) /\ (Int (Cl (B \/ C))) by A19, TOPS_1:def 8
.= Int (Cl (D /\ (E \/ F))) by A19, A20, A21, A22, Th7
.= Int (Cl ((A /\ B) \/ (A /\ C))) by A19, A20, A21, XBOOLE_1:23
.= (a "/\" b) "\/" (a "/\" c) by A24, A25, Def10 ; :: thesis: verum
end;
end;
hence LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice ; :: thesis: verum