:: TDLAT_1 semantic presentation begin theorem Th1: :: TDLAT_1:1 for T being 1-sorted for A, B being Subset of T holds ( A \/ B = [#] T iff A ` c= B ) proof let T be 1-sorted ; ::_thesis: for A, B being Subset of T holds ( A \/ B = [#] T iff A ` c= B ) let A, B be Subset of T; ::_thesis: ( A \/ B = [#] T iff A ` c= B ) hereby ::_thesis: ( A ` c= B implies A \/ B = [#] T ) assume A \/ B = [#] T ; ::_thesis: A ` c= B then ([#] T) \ A = B \ A by XBOOLE_1:40; hence A ` c= B by XBOOLE_1:36; ::_thesis: verum end; assume A ` c= B ; ::_thesis: A \/ B = [#] T then A \/ (A `) c= A \/ B by XBOOLE_1:9; then [#] T c= A \/ B by PRE_TOPC:2; hence A \/ B = [#] T by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th2: :: TDLAT_1:2 for T being 1-sorted for A, B being Subset of T holds ( A misses B iff B c= A ` ) by SUBSET_1:23; theorem Th3: :: TDLAT_1:3 for T being TopSpace for A being Subset of T holds Cl (Int (Cl A)) c= Cl A proof let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (Int (Cl A)) c= Cl A let A be Subset of T; ::_thesis: Cl (Int (Cl A)) c= Cl A Cl (Int (Cl A)) c= Cl (Cl A) by PRE_TOPC:19, TOPS_1:16; hence Cl (Int (Cl A)) c= Cl A ; ::_thesis: verum end; theorem Th4: :: TDLAT_1:4 for T being TopSpace for A being Subset of T holds Int A c= Int (Cl (Int A)) proof let T be TopSpace; ::_thesis: for A being Subset of T holds Int A c= Int (Cl (Int A)) let A be Subset of T; ::_thesis: Int A c= Int (Cl (Int A)) Int (Int A) c= Int (Cl (Int A)) by PRE_TOPC:18, TOPS_1:19; hence Int A c= Int (Cl (Int A)) ; ::_thesis: verum end; theorem Th5: :: TDLAT_1:5 for T being TopSpace for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A))) proof let T be TopSpace; ::_thesis: for A being Subset of T holds Int (Cl A) = Int (Cl (Int (Cl A))) let A be Subset of T; ::_thesis: Int (Cl A) = Int (Cl (Int (Cl A))) A1: Int (Int (Cl A)) c= Int (Cl (Int (Cl A))) by PRE_TOPC:18, TOPS_1:19; Int (Cl (Int (Cl A))) c= Int (Cl A) by Th3, TOPS_1:19; hence Int (Cl A) = Int (Cl (Int (Cl A))) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th6: :: TDLAT_1:6 for T being TopSpace for A, B being Subset of T st ( A is closed or B is closed ) holds (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) proof let T be TopSpace; ::_thesis: for A, B being Subset of T st ( A is closed or B is closed ) holds (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) let A, B be Subset of T; ::_thesis: ( ( A is closed or B is closed ) implies (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) ) A1: (A \/ B) \/ ((A \/ B) `) c= (A \/ B) \/ (Cl ((A \/ B) `)) by PRE_TOPC:18, XBOOLE_1:9; (A \/ B) \/ ((A \/ B) `) = [#] T by PRE_TOPC:2; then A2: (A \/ B) \/ (Cl ((A \/ B) `)) = [#] T by A1, XBOOLE_0:def_10; then A \/ (B \/ (Cl ((A \/ B) `))) = [#] T by XBOOLE_1:4; then A ` c= B \/ (Cl ((A \/ B) `)) by Th1; then A3: Cl (A `) c= Cl (B \/ (Cl ((A \/ B) `))) by PRE_TOPC:19; B \/ (A \/ (Cl ((A \/ B) `))) = [#] T by A2, XBOOLE_1:4; then B ` c= A \/ (Cl ((A \/ B) `)) by Th1; then A4: Cl (B `) c= Cl (A \/ (Cl ((A \/ B) `))) by PRE_TOPC:19; assume A5: ( A is closed or B is closed ) ; ::_thesis: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) A6: now__::_thesis:_Cl_(Int_(A_\/_B))_c=_(Cl_(Int_A))_\/_(Cl_(Int_B)) percases ( A is closed or B is closed ) by A5; suppose A is closed ; ::_thesis: Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) then ((Cl (B `)) `) ` c= A \/ (Cl ((B \/ A) `)) by A4, PRE_TOPC:22; then ((Cl (B `)) `) \/ (A \/ (Cl ((B \/ A) `))) = [#] T by Th1; then (Int B) \/ (A \/ (Cl ((B \/ A) `))) = [#] T by TOPS_1:def_1; then A \/ ((Int B) \/ (Cl ((B \/ A) `))) = [#] T by XBOOLE_1:4; then A ` c= (Int B) \/ (Cl ((B \/ A) `)) by Th1; then Cl (A `) c= Cl ((Int B) \/ (Cl ((B \/ A) `))) by PRE_TOPC:19; then Cl (A `) c= (Cl (Int B)) \/ (Cl (Cl ((B \/ A) `))) by PRE_TOPC:20; then (Cl (A `)) \/ ((Cl (A `)) `) c= ((Cl (Int B)) \/ (Cl ((B \/ A) `))) \/ ((Cl (A `)) `) by XBOOLE_1:9; then [#] T c= ((Cl (Int B)) \/ (Cl ((B \/ A) `))) \/ ((Cl (A `)) `) by PRE_TOPC:2; then [#] T c= ((Cl ((B \/ A) `)) \/ (Cl (Int B))) \/ (Int A) by TOPS_1:def_1; then [#] T c= (Cl ((B \/ A) `)) \/ ((Cl (Int B)) \/ (Int A)) by XBOOLE_1:4; then [#] T = (Cl ((B \/ A) `)) \/ ((Cl (Int B)) \/ (Int A)) by XBOOLE_0:def_10; then (Cl ((B \/ A) `)) ` c= (Cl (Int B)) \/ (Int A) by Th1; then Int (B \/ A) c= (Cl (Int B)) \/ (Int A) by TOPS_1:def_1; then Cl (Int (B \/ A)) c= Cl ((Cl (Int B)) \/ (Int A)) by PRE_TOPC:19; then Cl (Int (B \/ A)) c= (Cl (Cl (Int B))) \/ (Cl (Int A)) by PRE_TOPC:20; hence Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) ; ::_thesis: verum end; suppose B is closed ; ::_thesis: Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) then ((Cl (A `)) `) ` c= B \/ (Cl ((A \/ B) `)) by A3, PRE_TOPC:22; then ((Cl (A `)) `) \/ (B \/ (Cl ((A \/ B) `))) = [#] T by Th1; then (Int A) \/ (B \/ (Cl ((A \/ B) `))) = [#] T by TOPS_1:def_1; then B \/ ((Int A) \/ (Cl ((A \/ B) `))) = [#] T by XBOOLE_1:4; then B ` c= (Int A) \/ (Cl ((A \/ B) `)) by Th1; then Cl (B `) c= Cl ((Int A) \/ (Cl ((A \/ B) `))) by PRE_TOPC:19; then Cl (B `) c= (Cl (Int A)) \/ (Cl (Cl ((A \/ B) `))) by PRE_TOPC:20; then (Cl (B `)) \/ ((Cl (B `)) `) c= ((Cl (Int A)) \/ (Cl ((A \/ B) `))) \/ ((Cl (B `)) `) by XBOOLE_1:9; then [#] T c= ((Cl (Int A)) \/ (Cl ((A \/ B) `))) \/ ((Cl (B `)) `) by PRE_TOPC:2; then [#] T c= ((Cl ((A \/ B) `)) \/ (Cl (Int A))) \/ (Int B) by TOPS_1:def_1; then [#] T c= (Cl ((A \/ B) `)) \/ ((Cl (Int A)) \/ (Int B)) by XBOOLE_1:4; then [#] T = (Cl ((A \/ B) `)) \/ ((Cl (Int A)) \/ (Int B)) by XBOOLE_0:def_10; then (Cl ((A \/ B) `)) ` c= (Cl (Int A)) \/ (Int B) by Th1; then Int (A \/ B) c= (Cl (Int A)) \/ (Int B) by TOPS_1:def_1; then Cl (Int (A \/ B)) c= Cl ((Cl (Int A)) \/ (Int B)) by PRE_TOPC:19; then Cl (Int (A \/ B)) c= (Cl (Cl (Int A))) \/ (Cl (Int B)) by PRE_TOPC:20; hence Cl (Int (A \/ B)) c= (Cl (Int A)) \/ (Cl (Int B)) ; ::_thesis: verum end; end; end; Int B c= Int (A \/ B) by TOPS_1:19, XBOOLE_1:7; then A7: Cl (Int B) c= Cl (Int (A \/ B)) by PRE_TOPC:19; Int A c= Int (A \/ B) by TOPS_1:19, XBOOLE_1:7; then Cl (Int A) c= Cl (Int (A \/ B)) by PRE_TOPC:19; then (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by A7, XBOOLE_1:8; hence (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B)) by A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th7: :: TDLAT_1:7 for T being TopSpace for A, B being Subset of T st ( A is open or B is open ) holds (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) proof let T be TopSpace; ::_thesis: for A, B being Subset of T st ( A is open or B is open ) holds (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) let A, B be Subset of T; ::_thesis: ( ( A is open or B is open ) implies (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) ) A1: Int (A `) misses (Int (A `)) ` by XBOOLE_1:79; A2: Int (B `) misses (Int (B `)) ` by XBOOLE_1:79; A /\ B misses (A /\ B) ` by XBOOLE_1:79; then A3: {} T = (A /\ B) /\ ((A /\ B) `) by XBOOLE_0:def_7; A4: (A /\ B) /\ (Int ((A /\ B) `)) c= (A /\ B) /\ ((A /\ B) `) by TOPS_1:16, XBOOLE_1:26; then A /\ (B /\ (Int ((A /\ B) `))) = {} T by A3, XBOOLE_1:16; then A misses B /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7; then B /\ (Int ((A /\ B) `)) c= A ` by Th2; then A5: Int (B /\ (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:19; B /\ (A /\ (Int ((A /\ B) `))) = {} T by A3, A4, XBOOLE_1:16; then B misses A /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7; then A /\ (Int ((A /\ B) `)) c= B ` by Th2; then A6: Int (A /\ (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:19; assume A7: ( A is open or B is open ) ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) A8: now__::_thesis:_(Int_(Cl_A))_/\_(Int_(Cl_B))_c=_Int_(Cl_(A_/\_B)) percases ( A is open or B is open ) by A7; suppose A is open ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) then A /\ (Int ((A /\ B) `)) c= ((Int (B `)) `) ` by A6, TOPS_1:23; then (Int (B `)) ` misses A /\ (Int ((A /\ B) `)) by Th2; then ((Int (B `)) `) /\ (A /\ (Int ((A /\ B) `))) = {} by XBOOLE_0:def_7; then (((Cl ((B `) `)) `) `) /\ (A /\ (Int ((A /\ B) `))) = {} by TOPS_1:def_1; then A /\ ((Cl B) /\ (Int ((A /\ B) `))) = {} by XBOOLE_1:16; then A misses (Cl B) /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7; then (Cl B) /\ (Int ((A /\ B) `)) c= A ` by Th2; then Int ((Cl B) /\ (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:19; then (Int (Cl B)) /\ (Int (Int ((A /\ B) `))) c= Int (A `) by TOPS_1:17; then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ ((Int (A `)) `) c= (Int (A `)) /\ ((Int (A `)) `) by XBOOLE_1:26; then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ ((Int (A `)) `) c= {} T by A1, XBOOLE_0:def_7; then ((Int (Cl B)) /\ (Int ((A /\ B) `))) /\ (((Cl ((A `) `)) `) `) c= {} T by TOPS_1:def_1; then {} T = (Int ((A /\ B) `)) /\ ((Int (Cl B)) /\ (Cl A)) by XBOOLE_1:16; then Int ((A /\ B) `) misses (Int (Cl B)) /\ (Cl A) by XBOOLE_0:def_7; then (Int (Cl B)) /\ (Cl A) c= (Int ((A /\ B) `)) ` by Th2; then (Int (Cl B)) /\ (Cl A) c= ((Cl (((A /\ B) `) `)) `) ` by TOPS_1:def_1; then Int ((Int (Cl B)) /\ (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:19; then (Int (Int (Cl B))) /\ (Int (Cl A)) c= Int (Cl (B /\ A)) by TOPS_1:17; hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; ::_thesis: verum end; suppose B is open ; ::_thesis: (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) then B /\ (Int ((A /\ B) `)) c= ((Int (A `)) `) ` by A5, TOPS_1:23; then (Int (A `)) ` misses B /\ (Int ((A /\ B) `)) by Th2; then ((Int (A `)) `) /\ (B /\ (Int ((A /\ B) `))) = {} T by XBOOLE_0:def_7; then (((Cl ((A `) `)) `) `) /\ (B /\ (Int ((A /\ B) `))) = {} T by TOPS_1:def_1; then B /\ ((Cl A) /\ (Int ((A /\ B) `))) = {} T by XBOOLE_1:16; then B misses (Cl A) /\ (Int ((A /\ B) `)) by XBOOLE_0:def_7; then (Cl A) /\ (Int ((A /\ B) `)) c= B ` by Th2; then Int ((Cl A) /\ (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:19; then (Int (Cl A)) /\ (Int (Int ((A /\ B) `))) c= Int (B `) by TOPS_1:17; then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ ((Int (B `)) `) c= (Int (B `)) /\ ((Int (B `)) `) by XBOOLE_1:26; then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ ((Int (B `)) `) c= {} T by A2, XBOOLE_0:def_7; then ((Int (Cl A)) /\ (Int ((A /\ B) `))) /\ (((Cl ((B `) `)) `) `) c= {} T by TOPS_1:def_1; then {} T = (Int ((A /\ B) `)) /\ ((Int (Cl A)) /\ (Cl B)) by XBOOLE_1:16; then Int ((A /\ B) `) misses (Int (Cl A)) /\ (Cl B) by XBOOLE_0:def_7; then (Int (Cl A)) /\ (Cl B) c= (Int ((A /\ B) `)) ` by Th2; then (Int (Cl A)) /\ (Cl B) c= ((Cl (((A /\ B) `) `)) `) ` by TOPS_1:def_1; then Int ((Int (Cl A)) /\ (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:19; then (Int (Int (Cl A))) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) by TOPS_1:17; hence (Int (Cl A)) /\ (Int (Cl B)) c= Int (Cl (A /\ B)) ; ::_thesis: verum end; end; end; Cl (A /\ B) c= Cl B by PRE_TOPC:19, XBOOLE_1:17; then A9: Int (Cl (A /\ B)) c= Int (Cl B) by TOPS_1:19; Cl (A /\ B) c= Cl A by PRE_TOPC:19, XBOOLE_1:17; then Int (Cl (A /\ B)) c= Int (Cl A) by TOPS_1:19; then Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by A9, XBOOLE_1:19; hence (Int (Cl A)) /\ (Int (Cl B)) = Int (Cl (A /\ B)) by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th8: :: TDLAT_1:8 for T being TopSpace for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T proof let T be TopSpace; ::_thesis: for A being Subset of T holds Int (A /\ (Cl (A `))) = {} T let A be Subset of T; ::_thesis: Int (A /\ (Cl (A `))) = {} T A1: Int A misses (Int A) ` by XBOOLE_1:79; thus Int (A /\ (Cl (A `))) = Int (A /\ (((Cl (A `)) `) `)) .= Int (A /\ ((Int A) `)) by TOPS_1:def_1 .= (Int (Int A)) /\ (Int ((Int A) `)) by TOPS_1:17 .= Int ((Int A) /\ ((Int A) `)) by TOPS_1:17 .= Int ({} T) by A1, XBOOLE_0:def_7 .= {} T ; ::_thesis: verum end; theorem Th9: :: TDLAT_1:9 for T being TopSpace for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T proof let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (A \/ (Int (A `))) = [#] T let A be Subset of T; ::_thesis: Cl (A \/ (Int (A `))) = [#] T thus Cl (A \/ (Int (A `))) = Cl (A \/ ((Cl ((A `) `)) `)) by TOPS_1:def_1 .= (Cl (Cl A)) \/ (Cl ((Cl A) `)) by PRE_TOPC:20 .= Cl ((Cl A) \/ ((Cl A) `)) by PRE_TOPC:20 .= Cl ([#] T) by PRE_TOPC:2 .= [#] T by TOPS_1:2 ; ::_thesis: verum end; theorem Th10: :: TDLAT_1:10 for T being TopSpace for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) proof let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) let A, B be Subset of T; ::_thesis: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) Cl B c= Cl (A \/ B) by PRE_TOPC:19, XBOOLE_1:7; then A1: Int (Cl B) c= Int (Cl (A \/ B)) by TOPS_1:19; A \/ B c= A \/ ((Int (Cl B)) \/ B) by XBOOLE_1:7, XBOOLE_1:9; then Cl (A \/ B) c= Cl (A \/ ((Int (Cl B)) \/ B)) by PRE_TOPC:19; then A2: Int (Cl (A \/ B)) c= Int (Cl (A \/ ((Int (Cl B)) \/ B))) by TOPS_1:19; Int (Cl (A \/ ((Int (Cl B)) \/ B))) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by XBOOLE_1:7; then A3: Int (Cl (A \/ B)) c= (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) by A2, XBOOLE_1:1; Int (Cl (A \/ ((Int (Cl B)) \/ B))) = Int (Cl ((A \/ (Int (Cl B))) \/ B)) by XBOOLE_1:4 .= Int ((Cl (A \/ (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:20 .= Int (((Cl A) \/ (Cl (Int (Cl B)))) \/ (Cl B)) by PRE_TOPC:20 .= Int ((Cl A) \/ ((Cl (Int (Cl B))) \/ (Cl B))) by XBOOLE_1:4 .= Int ((Cl A) \/ (Cl B)) by Th3, XBOOLE_1:12 .= Int (Cl (A \/ B)) by PRE_TOPC:20 ; then (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) c= Int (Cl (A \/ B)) by A1, XBOOLE_1:8; then A4: (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (Int (Cl B)) = Int (Cl (A \/ B)) by A3, XBOOLE_0:def_10; A \/ ((Int (Cl B)) \/ B) = (Int (Cl B)) \/ (A \/ B) by XBOOLE_1:4; hence (Int (Cl (A \/ ((Int (Cl B)) \/ B)))) \/ (A \/ ((Int (Cl B)) \/ B)) = (Int (Cl (A \/ B))) \/ (A \/ B) by A4, XBOOLE_1:4; ::_thesis: verum end; theorem :: TDLAT_1:11 for T being TopSpace for A, C being Subset of T holds (Int (Cl (((Int (Cl A)) \/ A) \/ C))) \/ (((Int (Cl A)) \/ A) \/ C) = (Int (Cl (A \/ C))) \/ (A \/ C) by Th10; theorem Th12: :: TDLAT_1:12 for T being TopSpace for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B) proof let T be TopSpace; ::_thesis: for A, B being Subset of T holds (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B) let A, B be Subset of T; ::_thesis: (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B) Int (A /\ B) c= Int B by TOPS_1:19, XBOOLE_1:17; then A1: Cl (Int (A /\ B)) c= Cl (Int B) by PRE_TOPC:19; Cl (Int (A /\ ((Cl (Int B)) /\ B))) = Cl (Int ((A /\ (Cl (Int B))) /\ B)) by XBOOLE_1:16 .= Cl ((Int (A /\ (Cl (Int B)))) /\ (Int B)) by TOPS_1:17 .= Cl (((Int A) /\ (Int (Cl (Int B)))) /\ (Int B)) by TOPS_1:17 .= Cl ((Int A) /\ ((Int (Cl (Int B))) /\ (Int B))) by XBOOLE_1:16 .= Cl ((Int A) /\ (Int B)) by Th4, XBOOLE_1:28 .= Cl (Int (A /\ B)) by TOPS_1:17 ; then A2: Cl (Int (A /\ B)) c= (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) by A1, XBOOLE_1:19; A /\ ((Cl (Int B)) /\ B) c= A /\ B by XBOOLE_1:17, XBOOLE_1:26; then Int (A /\ ((Cl (Int B)) /\ B)) c= Int (A /\ B) by TOPS_1:19; then A3: Cl (Int (A /\ ((Cl (Int B)) /\ B))) c= Cl (Int (A /\ B)) by PRE_TOPC:19; (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ ((Cl (Int B)) /\ B))) by XBOOLE_1:17; then (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) c= Cl (Int (A /\ B)) by A3, XBOOLE_1:1; then A4: (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (Cl (Int B)) = Cl (Int (A /\ B)) by A2, XBOOLE_0:def_10; A /\ ((Cl (Int B)) /\ B) = (Cl (Int B)) /\ (A /\ B) by XBOOLE_1:16; hence (Cl (Int (A /\ ((Cl (Int B)) /\ B)))) /\ (A /\ ((Cl (Int B)) /\ B)) = (Cl (Int (A /\ B))) /\ (A /\ B) by A4, XBOOLE_1:16; ::_thesis: verum end; theorem :: TDLAT_1:13 for T being TopSpace for A, C being Subset of T holds (Cl (Int (((Cl (Int A)) /\ A) /\ C))) /\ (((Cl (Int A)) /\ A) /\ C) = (Cl (Int (A /\ C))) /\ (A /\ C) by Th12; begin theorem Th14: :: TDLAT_1:14 for T being TopSpace holds {} T is condensed proof let T be TopSpace; ::_thesis: {} T is condensed Int ({} T) c= {} T ; then A1: Int (Cl ({} T)) c= {} T by PRE_TOPC:22; {} T c= Cl (Int ({} T)) by PRE_TOPC:18; hence {} T is condensed by A1, TOPS_1:def_6; ::_thesis: verum end; theorem Th15: :: TDLAT_1:15 for T being TopSpace holds [#] T is condensed proof let T be TopSpace; ::_thesis: [#] T is condensed [#] T c= Cl ([#] T) by PRE_TOPC:18; then A1: [#] T c= Cl (Int ([#] T)) by TOPS_1:15; Int (Cl ([#] T)) c= [#] T ; hence [#] T is condensed by A1, TOPS_1:def_6; ::_thesis: verum end; theorem Th16: :: TDLAT_1:16 for T being TopSpace for A being Subset of T st A is condensed holds A ` is condensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds A ` is condensed let X be Subset of T; ::_thesis: ( X is condensed implies X ` is condensed ) assume A1: X is condensed ; ::_thesis: X ` is condensed then X c= Cl (Int X) by TOPS_1:def_6; then (Cl (((Int X) `) `)) ` c= X ` by SUBSET_1:12; then Int ((Int X) `) c= X ` by TOPS_1:def_1; then A2: Int (((Cl (X `)) `) `) c= X ` by TOPS_1:def_1; Int (Cl X) c= X by A1, TOPS_1:def_6; then (Cl ((Cl X) `)) ` c= X by TOPS_1:def_1; then X ` c= Cl ((Cl ((X `) `)) `) by SUBSET_1:12; then X ` c= Cl (Int (X `)) by TOPS_1:def_1; hence X ` is condensed by A2, TOPS_1:def_6; ::_thesis: verum end; theorem Th17: :: TDLAT_1:17 for T being TopSpace for A, B being Subset of T st A is condensed & B is condensed holds ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) proof let T be TopSpace; ::_thesis: for A, B being Subset of T st A is condensed & B is condensed holds ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) let A, B be Subset of T; ::_thesis: ( A is condensed & B is condensed implies ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) ) assume A1: A is condensed ; ::_thesis: ( not B is condensed or ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) ) assume A2: B is condensed ; ::_thesis: ( (Int (Cl (A \/ B))) \/ (A \/ B) is condensed & (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ) then A3: B c= Cl (Int B) by TOPS_1:def_6; A4: A c= Cl (Int A) by A1, TOPS_1:def_6; thus (Int (Cl (A \/ B))) \/ (A \/ B) is condensed ::_thesis: (Cl (Int (A /\ B))) /\ (A /\ B) is condensed proof set X = (Int (Cl (A \/ B))) \/ (A \/ B); Cl ((Int A) \/ (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:19, TOPS_1:20; then A5: (Cl (Int A)) \/ (Cl (Int B)) c= Cl (Int (A \/ B)) by PRE_TOPC:20; A \/ B c= (Cl (Int A)) \/ (Cl (Int B)) by A4, A3, XBOOLE_1:13; then A \/ B c= Cl (Int (A \/ B)) by A5, XBOOLE_1:1; then A6: (Int (Cl (A \/ B))) \/ (A \/ B) c= (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) by XBOOLE_1:9; Cl ((Int (Int (Cl (A \/ B)))) \/ (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:19, TOPS_1:20; then A7: (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by PRE_TOPC:20; Cl (Int (Cl (A \/ B))) c= Cl (Cl (A \/ B)) by PRE_TOPC:19, TOPS_1:16; then (Cl (Int (Cl (A \/ B)))) \/ (Cl (A \/ B)) = Cl (A \/ B) by XBOOLE_1:12; then Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) = Int (Cl (A \/ B)) by PRE_TOPC:20; then A8: Int (Cl ((Int (Cl (A \/ B))) \/ (A \/ B))) c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7; (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= (Cl (Int (Cl (A \/ B)))) \/ (Cl (Int (A \/ B))) by PRE_TOPC:18, XBOOLE_1:9; then (Int (Cl (A \/ B))) \/ (Cl (Int (A \/ B))) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A7, XBOOLE_1:1; then (Int (Cl (A \/ B))) \/ (A \/ B) c= Cl (Int ((Int (Cl (A \/ B))) \/ (A \/ B))) by A6, XBOOLE_1:1; hence (Int (Cl (A \/ B))) \/ (A \/ B) is condensed by A8, TOPS_1:def_6; ::_thesis: verum end; A9: Int (Cl B) c= B by A2, TOPS_1:def_6; A10: Int (Cl A) c= A by A1, TOPS_1:def_6; thus (Cl (Int (A /\ B))) /\ (A /\ B) is condensed ::_thesis: verum proof set X = (Cl (Int (A /\ B))) /\ (A /\ B); Int (Cl (A /\ B)) c= Int ((Cl A) /\ (Cl B)) by PRE_TOPC:21, TOPS_1:19; then A11: Int (Cl (A /\ B)) c= (Int (Cl A)) /\ (Int (Cl B)) by TOPS_1:17; (Int (Cl A)) /\ (Int (Cl B)) c= A /\ B by A10, A9, XBOOLE_1:27; then Int (Cl (A /\ B)) c= A /\ B by A11, XBOOLE_1:1; then A12: (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by XBOOLE_1:26; Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= Int ((Cl (Cl (Int (A /\ B)))) /\ (Cl (A /\ B))) by PRE_TOPC:21, TOPS_1:19; then A13: Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) by TOPS_1:17; Int (Int (A /\ B)) c= Int (Cl (Int (A /\ B))) by PRE_TOPC:18, TOPS_1:19; then Int (A /\ B) = (Int (Cl (Int (A /\ B)))) /\ (Int (A /\ B)) by XBOOLE_1:28; then Cl (Int (A /\ B)) = Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by TOPS_1:17; then A14: (Cl (Int (A /\ B))) /\ (A /\ B) c= Cl (Int ((Cl (Int (A /\ B))) /\ (A /\ B))) by XBOOLE_1:17; (Int (Cl (Int (A /\ B)))) /\ (Int (Cl (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by TOPS_1:16, XBOOLE_1:26; then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (Int (Cl (A /\ B))) by A13, XBOOLE_1:1; then Int (Cl ((Cl (Int (A /\ B))) /\ (A /\ B))) c= (Cl (Int (A /\ B))) /\ (A /\ B) by A12, XBOOLE_1:1; hence (Cl (Int (A /\ B))) /\ (A /\ B) is condensed by A14, TOPS_1:def_6; ::_thesis: verum end; end; theorem Th18: :: TDLAT_1:18 for T being TopSpace holds {} T is closed_condensed proof let T be TopSpace; ::_thesis: {} T is closed_condensed Cl (Int ({} T)) = {} T by PRE_TOPC:22; hence {} T is closed_condensed by TOPS_1:def_7; ::_thesis: verum end; theorem Th19: :: TDLAT_1:19 for T being TopSpace holds [#] T is closed_condensed proof let T be TopSpace; ::_thesis: [#] T is closed_condensed Int ([#] T) = [#] T by TOPS_1:15; then Cl (Int ([#] T)) = [#] T by TOPS_1:2; hence [#] T is closed_condensed by TOPS_1:def_7; ::_thesis: verum end; theorem Th20: :: TDLAT_1:20 for T being TopSpace holds {} T is open_condensed proof let T be TopSpace; ::_thesis: {} T is open_condensed Cl ({} T) = {} T by PRE_TOPC:22; then Int (Cl ({} T)) = {} T ; hence {} T is open_condensed by TOPS_1:def_8; ::_thesis: verum end; theorem Th21: :: TDLAT_1:21 for T being TopSpace holds [#] T is open_condensed proof let T be TopSpace; ::_thesis: [#] T is open_condensed Cl ([#] T) = [#] T by TOPS_1:2; then Int (Cl ([#] T)) = [#] T by TOPS_1:15; hence [#] T is open_condensed by TOPS_1:def_8; ::_thesis: verum end; theorem Th22: :: TDLAT_1:22 for T being TopSpace for A being Subset of T holds Cl (Int A) is closed_condensed proof let T be TopSpace; ::_thesis: for A being Subset of T holds Cl (Int A) is closed_condensed let A be Subset of T; ::_thesis: Cl (Int A) is closed_condensed Cl (Int A) = Cl (Int (Cl (Int A))) by TOPS_1:26; hence Cl (Int A) is closed_condensed by TOPS_1:def_7; ::_thesis: verum end; theorem Th23: :: TDLAT_1:23 for T being TopSpace for A being Subset of T holds Int (Cl A) is open_condensed proof let T be TopSpace; ::_thesis: for A being Subset of T holds Int (Cl A) is open_condensed let A be Subset of T; ::_thesis: Int (Cl A) is open_condensed Int (Cl A) = Int (Cl (Int (Cl A))) by Th5; hence Int (Cl A) is open_condensed by TOPS_1:def_8; ::_thesis: verum end; theorem Th24: :: TDLAT_1:24 for T being TopSpace for A being Subset of T st A is condensed holds Cl A is closed_condensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds Cl A is closed_condensed let A be Subset of T; ::_thesis: ( A is condensed implies Cl A is closed_condensed ) assume A1: A is condensed ; ::_thesis: Cl A is closed_condensed then Int (Cl A) c= A by TOPS_1:def_6; then A2: Cl (Int (Cl A)) c= Cl A by PRE_TOPC:19; Cl A is condensed by A1, TOPS_1:71; then Cl A c= Cl (Int (Cl A)) by TOPS_1:def_6; then Cl A = Cl (Int (Cl A)) by A2, XBOOLE_0:def_10; hence Cl A is closed_condensed by TOPS_1:def_7; ::_thesis: verum end; theorem Th25: :: TDLAT_1:25 for T being TopSpace for A being Subset of T st A is condensed holds Int A is open_condensed proof let T be TopSpace; ::_thesis: for A being Subset of T st A is condensed holds Int A is open_condensed let A be Subset of T; ::_thesis: ( A is condensed implies Int A is open_condensed ) assume A1: A is condensed ; ::_thesis: Int A is open_condensed then A c= Cl (Int A) by TOPS_1:def_6; then A2: Int A c= Int (Cl (Int A)) by TOPS_1:19; Int A is condensed by A1, TOPS_1:71; then Int (Cl (Int A)) c= Int A by TOPS_1:def_6; then Int (Cl (Int A)) = Int A by A2, XBOOLE_0:def_10; hence Int A is open_condensed by TOPS_1:def_8; ::_thesis: verum end; theorem :: TDLAT_1:26 for T being TopSpace for A being Subset of T st A is condensed holds Cl (A `) is closed_condensed by Th16, Th24; theorem :: TDLAT_1:27 for T being TopSpace for A being Subset of T st A is condensed holds Int (A `) is open_condensed by Th16, Th25; theorem Th28: :: TDLAT_1:28 for T being TopSpace for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) proof let T be TopSpace; ::_thesis: for A, B, C being Subset of T st A is closed_condensed & B is closed_condensed & C is closed_condensed holds Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) let A, B, C be Subset of T; ::_thesis: ( A is closed_condensed & B is closed_condensed & C is closed_condensed implies Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) ) assume that A1: A is closed_condensed and A2: B is closed_condensed and A3: C is closed_condensed ; ::_thesis: Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) A4: B = Cl (Int B) by A2, TOPS_1:def_7; A5: (A /\ B) /\ C c= C by XBOOLE_1:17; A6: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (Cl (Int (B /\ C))) by TOPS_1:16; A7: Cl (Int (B /\ C)) = Cl ((Int B) /\ (Int C)) by TOPS_1:17; C = Cl (Int C) by A3, TOPS_1:def_7; then A /\ (Cl (Int (B /\ C))) c= A /\ (B /\ C) by A7, A4, PRE_TOPC:21, XBOOLE_1:26; then A8: Int (A /\ (Cl (Int (B /\ C)))) c= A /\ (B /\ C) by A6, XBOOLE_1:1; then Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by XBOOLE_1:16; then A9: Int (A /\ (Cl (Int (B /\ C)))) c= C by A5, XBOOLE_1:1; A10: (A /\ B) /\ C c= A /\ B by XBOOLE_1:17; Int (A /\ (Cl (Int (B /\ C)))) c= (A /\ B) /\ C by A8, XBOOLE_1:16; then Int (A /\ (Cl (Int (B /\ C)))) c= A /\ B by A10, XBOOLE_1:1; then A11: Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int (A /\ B) by TOPS_1:19; Int (A /\ B) c= Cl (Int (A /\ B)) by PRE_TOPC:18; then Int (A /\ (Cl (Int (B /\ C)))) c= Cl (Int (A /\ B)) by A11, XBOOLE_1:1; then Int (A /\ (Cl (Int (B /\ C)))) c= (Cl (Int (A /\ B))) /\ C by A9, XBOOLE_1:19; then Int (Int (A /\ (Cl (Int (B /\ C))))) c= Int ((Cl (Int (A /\ B))) /\ C) by TOPS_1:19; then A12: Cl (Int (A /\ (Cl (Int (B /\ C))))) c= Cl (Int ((Cl (Int (A /\ B))) /\ C)) by PRE_TOPC:19; A13: A /\ (B /\ C) c= B /\ C by XBOOLE_1:17; A14: A /\ (B /\ C) c= A by XBOOLE_1:17; A15: Int ((Cl (Int (A /\ B))) /\ C) c= (Cl (Int (A /\ B))) /\ C by TOPS_1:16; A16: Cl (Int (A /\ B)) = Cl ((Int A) /\ (Int B)) by TOPS_1:17; A = Cl (Int A) by A1, TOPS_1:def_7; then (Cl (Int (A /\ B))) /\ C c= (A /\ B) /\ C by A16, A4, PRE_TOPC:21, XBOOLE_1:26; then A17: Int ((Cl (Int (A /\ B))) /\ C) c= (A /\ B) /\ C by A15, XBOOLE_1:1; then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by XBOOLE_1:16; then A18: Int ((Cl (Int (A /\ B))) /\ C) c= A by A14, XBOOLE_1:1; Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (B /\ C) by A17, XBOOLE_1:16; then Int ((Cl (Int (A /\ B))) /\ C) c= B /\ C by A13, XBOOLE_1:1; then A19: Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (B /\ C) by TOPS_1:19; Int (B /\ C) c= Cl (Int (B /\ C)) by PRE_TOPC:18; then Int ((Cl (Int (A /\ B))) /\ C) c= Cl (Int (B /\ C)) by A19, XBOOLE_1:1; then Int ((Cl (Int (A /\ B))) /\ C) c= A /\ (Cl (Int (B /\ C))) by A18, XBOOLE_1:19; then Int (Int ((Cl (Int (A /\ B))) /\ C)) c= Int (A /\ (Cl (Int (B /\ C)))) by TOPS_1:19; then Cl (Int ((Cl (Int (A /\ B))) /\ C)) c= Cl (Int (A /\ (Cl (Int (B /\ C))))) by PRE_TOPC:19; hence Cl (Int (A /\ (Cl (Int (B /\ C))))) = Cl (Int ((Cl (Int (A /\ B))) /\ C)) by A12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: TDLAT_1:29 for T being TopSpace for A, B, C being Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) proof let T be TopSpace; ::_thesis: for A, B, C being Subset of T st A is open_condensed & B is open_condensed & C is open_condensed holds Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) let A, B, C be Subset of T; ::_thesis: ( A is open_condensed & B is open_condensed & C is open_condensed implies Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) ) assume that A1: A is open_condensed and A2: B is open_condensed and A3: C is open_condensed ; ::_thesis: Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) A4: B = Int (Cl B) by A2, TOPS_1:def_8; A5: C c= (A \/ B) \/ C by XBOOLE_1:7; A6: A \/ (Int (Cl (B \/ C))) c= Cl (A \/ (Int (Cl (B \/ C)))) by PRE_TOPC:18; A7: Int (Cl (B \/ C)) = Int ((Cl B) \/ (Cl C)) by PRE_TOPC:20; C = Int (Cl C) by A3, TOPS_1:def_8; then A \/ (B \/ C) c= A \/ (Int (Cl (B \/ C))) by A7, A4, TOPS_1:20, XBOOLE_1:9; then A8: A \/ (B \/ C) c= Cl (A \/ (Int (Cl (B \/ C)))) by A6, XBOOLE_1:1; then (A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by XBOOLE_1:4; then A9: C c= Cl (A \/ (Int (Cl (B \/ C)))) by A5, XBOOLE_1:1; A10: A \/ B c= (A \/ B) \/ C by XBOOLE_1:7; (A \/ B) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A8, XBOOLE_1:4; then A \/ B c= Cl (A \/ (Int (Cl (B \/ C)))) by A10, XBOOLE_1:1; then A11: Cl (A \/ B) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19; Int (Cl (A \/ B)) c= Cl (A \/ B) by TOPS_1:16; then Int (Cl (A \/ B)) c= Cl (A \/ (Int (Cl (B \/ C)))) by A11, XBOOLE_1:1; then (Int (Cl (A \/ B))) \/ C c= Cl (A \/ (Int (Cl (B \/ C)))) by A9, XBOOLE_1:8; then Cl ((Int (Cl (A \/ B))) \/ C) c= Cl (Cl (A \/ (Int (Cl (B \/ C))))) by PRE_TOPC:19; then A12: Int (Cl ((Int (Cl (A \/ B))) \/ C)) c= Int (Cl (A \/ (Int (Cl (B \/ C))))) by TOPS_1:19; A13: B \/ C c= A \/ (B \/ C) by XBOOLE_1:7; A14: A c= A \/ (B \/ C) by XBOOLE_1:7; A15: (Int (Cl (A \/ B))) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by PRE_TOPC:18; A16: Int (Cl (A \/ B)) = Int ((Cl A) \/ (Cl B)) by PRE_TOPC:20; A = Int (Cl A) by A1, TOPS_1:def_8; then (A \/ B) \/ C c= (Int (Cl (A \/ B))) \/ C by A16, A4, TOPS_1:20, XBOOLE_1:9; then A17: (A \/ B) \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A15, XBOOLE_1:1; then A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by XBOOLE_1:4; then A18: A c= Cl ((Int (Cl (A \/ B))) \/ C) by A14, XBOOLE_1:1; A \/ (B \/ C) c= Cl ((Int (Cl (A \/ B))) \/ C) by A17, XBOOLE_1:4; then B \/ C c= Cl ((Int (Cl (A \/ B))) \/ C) by A13, XBOOLE_1:1; then A19: Cl (B \/ C) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19; Int (Cl (B \/ C)) c= Cl (B \/ C) by TOPS_1:16; then Int (Cl (B \/ C)) c= Cl ((Int (Cl (A \/ B))) \/ C) by A19, XBOOLE_1:1; then A \/ (Int (Cl (B \/ C))) c= Cl ((Int (Cl (A \/ B))) \/ C) by A18, XBOOLE_1:8; then Cl (A \/ (Int (Cl (B \/ C)))) c= Cl (Cl ((Int (Cl (A \/ B))) \/ C)) by PRE_TOPC:19; then Int (Cl (A \/ (Int (Cl (B \/ C))))) c= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by TOPS_1:19; hence Int (Cl (A \/ (Int (Cl (B \/ C))))) = Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A12, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let T be TopStruct ; func Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 1 { A where A is Subset of T : A is condensed } ; coherence { A where A is Subset of T : A is condensed } is Subset-Family of T proof set B = { A where A is Subset of T : A is condensed } ; { A where A is Subset of T : A is condensed } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is condensed } or x in bool the carrier of T ) assume x in { A where A is Subset of T : A is condensed } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T st ( x = A & A is condensed ) ; hence x in bool the carrier of T ; ::_thesis: verum end; hence { A where A is Subset of T : A is condensed } is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines Domains_of TDLAT_1:def_1_:_ for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ; registration let T be TopSpace; cluster Domains_of T -> non empty ; coherence not Domains_of T is empty proof {} T is condensed by Th14; then {} T in { A where A is Subset of T : A is condensed } ; hence not Domains_of T is empty ; ::_thesis: verum end; end; definition let T be TopSpace; func Domains_Union T -> BinOp of (Domains_of T) means :Def2: :: TDLAT_1:def 2 for A, B being Element of Domains_of T holds it . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B); existence ex b1 being BinOp of (Domains_of T) st for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) proof defpred S1[ set , set ] means for A, B being Element of Domains_of T st $1 = [A,B] holds $2 = (Int (Cl (A \/ B))) \/ (A \/ B); set D = [:(Domains_of T),(Domains_of T):]; A1: for a being Element of [:(Domains_of T),(Domains_of T):] ex b being Element of Domains_of T st S1[a,b] proof let a be Element of [:(Domains_of T),(Domains_of T):]; ::_thesis: ex b being Element of Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Domains_of T ; F in { H where H is Subset of T : H is condensed } ; then A2: ex H being Subset of T st ( H = F & H is condensed ) ; G in { E where E is Subset of T : E is condensed } ; then ex E being Subset of T st ( E = G & E is condensed ) ; then (Int (Cl (G \/ F))) \/ (G \/ F) is condensed by A2, Th17; then (Int (Cl (G \/ F))) \/ (G \/ F) in { E where E is Subset of T : E is condensed } ; then reconsider b = (Int (Cl (G \/ F))) \/ (G \/ F) as Element of Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Domains_of T; ::_thesis: ( a = [A,B] implies b = (Int (Cl (A \/ B))) \/ (A \/ B) ) assume a = [A,B] ; ::_thesis: b = (Int (Cl (A \/ B))) \/ (A \/ B) then A3: [A,B] = [G,F] by MCART_1:21; then A4: B = F by XTUPLE_0:1; A = G by A3, XTUPLE_0:1; hence b = (Int (Cl (A \/ B))) \/ (A \/ B) by A4; ::_thesis: verum end; consider h being Function of [:(Domains_of T),(Domains_of T):],(Domains_of T) such that A5: for a being Element of [:(Domains_of T),(Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Domains_of T holds h . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) let A, B be Element of Domains_of T; ::_thesis: h . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) thus h . (A,B) = h . [A,B] .= (Int (Cl (A \/ B))) \/ (A \/ B) by A5 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ) holds b1 = b2 proof deffunc H1( Element of Domains_of T, Element of Domains_of T) -> Element of bool the carrier of T = (Int (Cl ($1 \/ $2))) \/ ($1 \/ $2); thus for o1, o2 being BinOp of (Domains_of T) st ( for a, b being Element of Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def2 defines Domains_Union TDLAT_1:def_2_:_ for T being TopSpace for b2 being BinOp of (Domains_of T) holds ( b2 = Domains_Union T iff for A, B being Element of Domains_of T holds b2 . (A,B) = (Int (Cl (A \/ B))) \/ (A \/ B) ); notation let T be TopSpace; synonym D-Union T for Domains_Union T; end; definition let T be TopSpace; func Domains_Meet T -> BinOp of (Domains_of T) means :Def3: :: TDLAT_1:def 3 for A, B being Element of Domains_of T holds it . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B); existence ex b1 being BinOp of (Domains_of T) st for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) proof defpred S1[ set , set ] means for A, B being Element of Domains_of T st $1 = [A,B] holds $2 = (Cl (Int (A /\ B))) /\ (A /\ B); set D = [:(Domains_of T),(Domains_of T):]; A1: for a being Element of [:(Domains_of T),(Domains_of T):] ex b being Element of Domains_of T st S1[a,b] proof let a be Element of [:(Domains_of T),(Domains_of T):]; ::_thesis: ex b being Element of Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Domains_of T ; F in { H where H is Subset of T : H is condensed } ; then A2: ex H being Subset of T st ( H = F & H is condensed ) ; G in { E where E is Subset of T : E is condensed } ; then ex E being Subset of T st ( E = G & E is condensed ) ; then (Cl (Int (G /\ F))) /\ (G /\ F) is condensed by A2, Th17; then (Cl (Int (G /\ F))) /\ (G /\ F) in { E where E is Subset of T : E is condensed } ; then reconsider b = (Cl (Int (G /\ F))) /\ (G /\ F) as Element of Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Domains_of T; ::_thesis: ( a = [A,B] implies b = (Cl (Int (A /\ B))) /\ (A /\ B) ) assume a = [A,B] ; ::_thesis: b = (Cl (Int (A /\ B))) /\ (A /\ B) then A3: [A,B] = [G,F] by MCART_1:21; then A4: B = F by XTUPLE_0:1; A = G by A3, XTUPLE_0:1; hence b = (Cl (Int (A /\ B))) /\ (A /\ B) by A4; ::_thesis: verum end; consider h being Function of [:(Domains_of T),(Domains_of T):],(Domains_of T) such that A5: for a being Element of [:(Domains_of T),(Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Domains_of T holds h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) let A, B be Element of Domains_of T; ::_thesis: h . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) thus h . (A,B) = h . [A,B] .= (Cl (Int (A /\ B))) /\ (A /\ B) by A5 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Domains_of T) st ( for A, B being Element of Domains_of T holds b1 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) & ( for A, B being Element of Domains_of T holds b2 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ) holds b1 = b2 proof deffunc H1( Element of Domains_of T, Element of Domains_of T) -> Element of bool the carrier of T = (Cl (Int ($1 /\ $2))) /\ ($1 /\ $2); thus for o1, o2 being BinOp of (Domains_of T) st ( for a, b being Element of Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def3 defines Domains_Meet TDLAT_1:def_3_:_ for T being TopSpace for b2 being BinOp of (Domains_of T) holds ( b2 = Domains_Meet T iff for A, B being Element of Domains_of T holds b2 . (A,B) = (Cl (Int (A /\ B))) /\ (A /\ B) ); notation let T be TopSpace; synonym D-Meet T for Domains_Meet T; end; theorem Th30: :: TDLAT_1:30 for T being TopSpace holds LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice proof let T be TopSpace; ::_thesis: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice set L = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); A1: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-commutative proof let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_4 ::_thesis: a "\/" b = b "\/" a reconsider A = a, B = b as Element of Domains_of T ; thus a "\/" b = (Int (Cl (B \/ A))) \/ (B \/ A) by Def2 .= b "\/" a by Def2 ; ::_thesis: verum end; A2: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-absorbing proof let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b reconsider A = a, B = b as Element of Domains_of T ; A3: (Cl (Int (A /\ B))) /\ (A /\ B) c= A /\ B by XBOOLE_1:17; B in { D where D is Subset of T : D is condensed } ; then ex D being Subset of T st ( D = B & D is condensed ) ; then A4: Int (Cl B) c= B by TOPS_1:def_6; A5: A /\ B c= B by XBOOLE_1:17; a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3; hence (a "/\" b) "\/" b = (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B) by Def2 .= (Int (Cl (((Cl (Int (A /\ B))) /\ (A /\ B)) \/ B))) \/ B by A3, A5, XBOOLE_1:1, XBOOLE_1:12 .= (Int (Cl B)) \/ B by A3, A5, XBOOLE_1:1, XBOOLE_1:12 .= b by A4, XBOOLE_1:12 ; ::_thesis: verum end; A6: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-associative proof let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_5 ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c reconsider A = a, B = b, C = c as Element of Domains_of T ; A7: a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2; b "\/" c = (Int (Cl (B \/ C))) \/ (B \/ C) by Def2; hence a "\/" (b "\/" c) = (Int (Cl (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))))) \/ (A \/ ((Int (Cl (B \/ C))) \/ (B \/ C))) by Def2 .= (Int (Cl (A \/ (B \/ C)))) \/ (A \/ (B \/ C)) by Th10 .= (Int (Cl (A \/ (B \/ C)))) \/ ((A \/ B) \/ C) by XBOOLE_1:4 .= (Int (Cl ((A \/ B) \/ C))) \/ ((A \/ B) \/ C) by XBOOLE_1:4 .= (Int (Cl (((Int (Cl (A \/ B))) \/ (A \/ B)) \/ C))) \/ (((Int (Cl (A \/ B))) \/ (A \/ B)) \/ C) by Th10 .= (a "\/" b) "\/" c by A7, Def2 ; ::_thesis: verum end; A8: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-commutative proof let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_6 ::_thesis: a "/\" b = b "/\" a reconsider A = a, B = b as Element of Domains_of T ; thus a "/\" b = (Cl (Int (B /\ A))) /\ (B /\ A) by Def3 .= b "/\" a by Def3 ; ::_thesis: verum end; A9: LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is join-absorbing proof let a, b be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a reconsider A = a, B = b as Element of Domains_of T ; A10: A c= A \/ B by XBOOLE_1:7; A in { D where D is Subset of T : D is condensed } ; then ex D being Subset of T st ( D = A & D is condensed ) ; then A11: A c= Cl (Int A) by TOPS_1:def_6; A12: A \/ B c= (Int (Cl (A \/ B))) \/ (A \/ B) by XBOOLE_1:7; a "\/" b = (Int (Cl (A \/ B))) \/ (A \/ B) by Def2; hence a "/\" (a "\/" b) = (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))) by Def3 .= (Cl (Int (A /\ ((Int (Cl (A \/ B))) \/ (A \/ B))))) /\ A by A10, A12, XBOOLE_1:1, XBOOLE_1:28 .= (Cl (Int A)) /\ A by A10, A12, XBOOLE_1:1, XBOOLE_1:28 .= a by A11, XBOOLE_1:28 ; ::_thesis: verum end; LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is meet-associative proof let a, b, c be Element of LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #); :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider A = a, B = b, C = c as Element of Domains_of T ; A13: a "/\" b = (Cl (Int (A /\ B))) /\ (A /\ B) by Def3; b "/\" c = (Cl (Int (B /\ C))) /\ (B /\ C) by Def3; hence a "/\" (b "/\" c) = (Cl (Int (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))))) /\ (A /\ ((Cl (Int (B /\ C))) /\ (B /\ C))) by Def3 .= (Cl (Int (A /\ (B /\ C)))) /\ (A /\ (B /\ C)) by Th12 .= (Cl (Int (A /\ (B /\ C)))) /\ ((A /\ B) /\ C) by XBOOLE_1:16 .= (Cl (Int ((A /\ B) /\ C))) /\ ((A /\ B) /\ C) by XBOOLE_1:16 .= (Cl (Int (((Cl (Int (A /\ B))) /\ (A /\ B)) /\ C))) /\ (((Cl (Int (A /\ B))) /\ (A /\ B)) /\ C) by Th12 .= (a "/\" b) "/\" c by A13, Def3 ; ::_thesis: verum end; then reconsider L = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) as Lattice by A1, A6, A2, A8, A9; A14: L is lower-bounded proof {} T is condensed by Th14; then {} T in { D where D is Subset of T : D is 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 Domains_of T ; C /\ A = C ; hence c "/\" a = (Cl (Int C)) /\ C by Def3 .= c ; ::_thesis: a "/\" c = c hence a "/\" c = c ; ::_thesis: verum end; L is upper-bounded proof [#] T is condensed by Th15; then [#] T in { D where D is Subset of T : D is 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 Domains_of T ; C \/ A = C by XBOOLE_1:12; hence c "\/" a = (Int (Cl C)) \/ C by Def2 .= c by XBOOLE_1:12 ; ::_thesis: a "\/" c = c hence a "\/" c = c ; ::_thesis: verum end; then reconsider L = L as 01_Lattice by A14; L is complemented proof [#] T is condensed by Th15; then [#] T in { D where D is Subset of T : D is 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 Domains_of T ; A15: B ` misses B by XBOOLE_1:79; B in { D where D is Subset of T : D is condensed } ; then ex D being Subset of T st ( D = B & D is condensed ) ; then B ` is condensed by Th16; then B ` in { D where D is Subset of T : D is condensed } ; then reconsider a = B ` as Element of L ; take a ; ::_thesis: a is_a_complement_of b A16: 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 Domains_of T ; V in { D where D is Subset of T : D is condensed } ; then ex D being Subset of T st ( D = V & D is condensed ) ; then A17: V c= Cl (Int V) by TOPS_1:def_6; thus the L_meet of L . (c,v) = (Cl (Int (([#] T) /\ V))) /\ (([#] T) /\ V) by Def3 .= (Cl (Int (([#] T) /\ V))) /\ V by XBOOLE_1:28 .= (Cl (Int V)) /\ V by XBOOLE_1:28 .= v by A17, XBOOLE_1:28 ; ::_thesis: verum end; thus a "\/" b = (Int (Cl ((B `) \/ B))) \/ ((B `) \/ B) by Def2 .= (Int (Cl ((B `) \/ B))) \/ ([#] T) by PRE_TOPC:2 .= c by XBOOLE_1:12 .= Top L by A16, 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 condensed by Th14; then {} T in { D where D is Subset of T : D is condensed } ; then reconsider c = {} T as Element of L ; A18: 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 Domains_of T ; V in { D where D is Subset of T : D is condensed } ; then ex D being Subset of T st ( D = V & D is condensed ) ; then A19: Int (Cl V) c= V by TOPS_1:def_6; thus the L_join of L . (c,v) = (Int (Cl (({} T) \/ V))) \/ (({} T) \/ V) by Def2 .= (Int (Cl ((([#] T) `) \/ V))) \/ (({} T) \/ V) by XBOOLE_1:37 .= (Int (Cl ((([#] T) `) \/ ((V `) `)))) \/ ((([#] T) `) \/ V) by XBOOLE_1:37 .= (Int (Cl ((([#] T) /\ (V `)) `))) \/ ((([#] T) `) \/ ((V `) `)) by XBOOLE_1:54 .= (Int (Cl ((([#] T) /\ (V `)) `))) \/ ((([#] T) /\ (V `)) `) by XBOOLE_1:54 .= (Int (Cl ((V `) `))) \/ ((([#] T) /\ (V `)) `) by XBOOLE_1:28 .= (Int (Cl V)) \/ ((V `) `) by XBOOLE_1:28 .= v by A19, XBOOLE_1:12 ; ::_thesis: verum end; thus a "/\" b = (Cl (Int ((B `) /\ B))) /\ ((B `) /\ B) by Def3 .= (Cl (Int ((B `) /\ B))) /\ ({} T) by A15, XBOOLE_0:def_7 .= Bottom L by A18, LATTICE2:15 ; ::_thesis: b "/\" a = Bottom L hence b "/\" a = Bottom L ; ::_thesis: verum end; hence LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) is C_Lattice ; ::_thesis: verum end; definition let T be TopSpace; func Domains_Lattice T -> C_Lattice equals :: TDLAT_1:def 4 LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #); coherence LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #) is C_Lattice by Th30; end; :: deftheorem defines Domains_Lattice TDLAT_1:def_4_:_ for T being TopSpace holds Domains_Lattice T = LattStr(# (Domains_of T),(Domains_Union T),(Domains_Meet T) #); begin definition let T be TopStruct ; func Closed_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 5 { A where A is Subset of T : A is closed_condensed } ; coherence { A where A is Subset of T : A is closed_condensed } is Subset-Family of T proof set B = { A where A is Subset of T : A is closed_condensed } ; { A where A is Subset of T : A is closed_condensed } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is closed_condensed } or x in bool the carrier of T ) assume x in { A where A is Subset of T : A is closed_condensed } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T st ( x = A & A is closed_condensed ) ; hence x in bool the carrier of T ; ::_thesis: verum end; hence { A where A is Subset of T : A is closed_condensed } is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines Closed_Domains_of TDLAT_1:def_5_:_ for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ; registration let T be TopSpace; cluster Closed_Domains_of T -> non empty ; coherence not Closed_Domains_of T is empty proof {} T is closed_condensed by Th18; then {} T in { A where A is Subset of T : A is closed_condensed } ; hence not Closed_Domains_of T is empty ; ::_thesis: verum end; end; theorem :: TDLAT_1:31 for T being TopSpace holds Closed_Domains_of T c= Domains_of T ; definition let T be TopSpace; func Closed_Domains_Union T -> BinOp of (Closed_Domains_of T) means :Def6: :: TDLAT_1:def 6 for A, B being Element of Closed_Domains_of T holds it . (A,B) = A \/ B; existence ex b1 being BinOp of (Closed_Domains_of T) st for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B proof defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds $2 = A \/ B; set D = [:(Closed_Domains_of T),(Closed_Domains_of T):]; A1: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] ex b being Element of Closed_Domains_of T st S1[a,b] proof let a be Element of [:(Closed_Domains_of T),(Closed_Domains_of T):]; ::_thesis: ex b being Element of Closed_Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Closed_Domains_of T ; G in { E where E is Subset of T : E is closed_condensed } ; then consider E being Subset of T such that A2: E = G and A3: E is closed_condensed ; F in { H where H is Subset of T : H is closed_condensed } ; then consider H being Subset of T such that A4: H = F and A5: H is closed_condensed ; E \/ H is closed_condensed by A3, A5, TOPS_1:68; then G \/ F in { K where K is Subset of T : K is closed_condensed } by A2, A4; then reconsider b = G \/ F as Element of Closed_Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = [A,B] implies b = A \/ B ) assume a = [A,B] ; ::_thesis: b = A \/ B then A6: [A,B] = [G,F] by MCART_1:21; then A = G by XTUPLE_0:1; hence b = A \/ B by A6, XTUPLE_0:1; ::_thesis: verum end; consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that A7: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Closed_Domains_of T holds h . (A,B) = A \/ B let A, B be Element of Closed_Domains_of T; ::_thesis: h . (A,B) = A \/ B thus h . (A,B) = h . [A,B] .= A \/ B by A7 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = A \/ B ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = A \/ B ) holds b1 = b2 proof deffunc H1( Element of Closed_Domains_of T, Element of Closed_Domains_of T) -> Element of bool the carrier of T = $1 \/ $2; thus for o1, o2 being BinOp of (Closed_Domains_of T) st ( for a, b being Element of Closed_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Closed_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def6 defines Closed_Domains_Union TDLAT_1:def_6_:_ for T being TopSpace for b2 being BinOp of (Closed_Domains_of T) holds ( b2 = Closed_Domains_Union T iff for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = A \/ B ); notation let T be TopSpace; synonym CLD-Union T for Closed_Domains_Union T; end; theorem Th32: :: TDLAT_1:32 for T being TopSpace for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B) proof let T be TopSpace; ::_thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Union T) . (A,B) = (D-Union T) . (A,B) let A, B be Element of Closed_Domains_of T; ::_thesis: (CLD-Union T) . (A,B) = (D-Union T) . (A,B) A1: A in { D where D is Subset of T : D is closed_condensed } ; reconsider A0 = A, B0 = B as Element of Domains_of T ; B in { E where E is Subset of T : E is closed_condensed } ; then consider E being Subset of T such that A2: E = B and A3: E is closed_condensed ; consider D being Subset of T such that A4: D = A and A5: D is closed_condensed by A1; D \/ E is closed_condensed by A5, A3, TOPS_1:68; then D \/ E is condensed by TOPS_1:66; then A6: Int (Cl (A \/ B)) c= A \/ B by A4, A2, TOPS_1:def_6; thus (CLD-Union T) . (A,B) = A \/ B by Def6 .= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A6, XBOOLE_1:12 .= (D-Union T) . (A,B) by Def2 ; ::_thesis: verum end; definition let T be TopSpace; func Closed_Domains_Meet T -> BinOp of (Closed_Domains_of T) means :Def7: :: TDLAT_1:def 7 for A, B being Element of Closed_Domains_of T holds it . (A,B) = Cl (Int (A /\ B)); existence ex b1 being BinOp of (Closed_Domains_of T) st for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B)) proof defpred S1[ set , set ] means for A, B being Element of Closed_Domains_of T st $1 = [A,B] holds $2 = Cl (Int (A /\ B)); set D = [:(Closed_Domains_of T),(Closed_Domains_of T):]; A1: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] ex b being Element of Closed_Domains_of T st S1[a,b] proof let a be Element of [:(Closed_Domains_of T),(Closed_Domains_of T):]; ::_thesis: ex b being Element of Closed_Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Closed_Domains_of T ; Cl (Int (G /\ F)) is closed_condensed by Th22; then Cl (Int (G /\ F)) in { E where E is Subset of T : E is closed_condensed } ; then reconsider b = Cl (Int (G /\ F)) as Element of Closed_Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Closed_Domains_of T; ::_thesis: ( a = [A,B] implies b = Cl (Int (A /\ B)) ) assume a = [A,B] ; ::_thesis: b = Cl (Int (A /\ B)) then A2: [A,B] = [G,F] by MCART_1:21; then A = G by XTUPLE_0:1; hence b = Cl (Int (A /\ B)) by A2, XTUPLE_0:1; ::_thesis: verum end; consider h being Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Closed_Domains_of T) such that A3: for a being Element of [:(Closed_Domains_of T),(Closed_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Closed_Domains_of T holds h . (A,B) = Cl (Int (A /\ B)) let A, B be Element of Closed_Domains_of T; ::_thesis: h . (A,B) = Cl (Int (A /\ B)) thus h . (A,B) = h . [A,B] .= Cl (Int (A /\ B)) by A3 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Closed_Domains_of T) st ( for A, B being Element of Closed_Domains_of T holds b1 . (A,B) = Cl (Int (A /\ B)) ) & ( for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) ) holds b1 = b2 proof deffunc H1( Element of Closed_Domains_of T, Element of Closed_Domains_of T) -> Element of bool the carrier of T = Cl (Int ($1 /\ $2)); thus for o1, o2 being BinOp of (Closed_Domains_of T) st ( for a, b being Element of Closed_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Closed_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def7 defines Closed_Domains_Meet TDLAT_1:def_7_:_ for T being TopSpace for b2 being BinOp of (Closed_Domains_of T) holds ( b2 = Closed_Domains_Meet T iff for A, B being Element of Closed_Domains_of T holds b2 . (A,B) = Cl (Int (A /\ B)) ); notation let T be TopSpace; synonym CLD-Meet T for Closed_Domains_Meet T; end; theorem Th33: :: TDLAT_1:33 for T being TopSpace for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B) proof let T be TopSpace; ::_thesis: for A, B being Element of Closed_Domains_of T holds (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B) let A, B be Element of Closed_Domains_of T; ::_thesis: (CLD-Meet T) . (A,B) = (D-Meet T) . (A,B) A in { D where D is Subset of T : D is closed_condensed } ; then consider D being Subset of T such that A1: D = A and A2: D is closed_condensed ; A3: Int (A /\ B) c= A /\ B by TOPS_1:16; reconsider A0 = A, B0 = B as Element of Domains_of T ; B in { E where E is Subset of T : E is closed_condensed } ; then consider E being Subset of T such that A4: E = B and A5: E is closed_condensed ; A6: E is closed by A5, TOPS_1:66; D is closed by A2, TOPS_1:66; then A7: Cl (D /\ E) = D /\ E by A6, PRE_TOPC:22; thus (CLD-Meet T) . (A,B) = Cl (Int (A /\ B)) by Def7 .= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A1, A4, A7, A3, PRE_TOPC:19, XBOOLE_1:28 .= (D-Meet T) . (A,B) by Def3 ; ::_thesis: verum end; theorem Th34: :: TDLAT_1:34 for T being TopSpace holds LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) is B_Lattice proof 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 end; definition let T be TopSpace; func Closed_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 8 LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #); coherence LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #) is B_Lattice by Th34; end; :: deftheorem defines Closed_Domains_Lattice TDLAT_1:def_8_:_ for T being TopSpace holds Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(Closed_Domains_Union T),(Closed_Domains_Meet T) #); begin definition let T be TopStruct ; func Open_Domains_of T -> Subset-Family of T equals :: TDLAT_1:def 9 { A where A is Subset of T : A is open_condensed } ; coherence { A where A is Subset of T : A is open_condensed } is Subset-Family of T proof set B = { A where A is Subset of T : A is open_condensed } ; { A where A is Subset of T : A is open_condensed } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : A is open_condensed } or x in bool the carrier of T ) assume x in { A where A is Subset of T : A is open_condensed } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T st ( x = A & A is open_condensed ) ; hence x in bool the carrier of T ; ::_thesis: verum end; hence { A where A is Subset of T : A is open_condensed } is Subset-Family of T ; ::_thesis: verum end; end; :: deftheorem defines Open_Domains_of TDLAT_1:def_9_:_ for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ; registration let T be TopSpace; cluster Open_Domains_of T -> non empty ; coherence not Open_Domains_of T is empty proof {} T is open_condensed by Th20; then {} T in { A where A is Subset of T : A is open_condensed } ; hence not Open_Domains_of T is empty ; ::_thesis: verum end; end; theorem :: TDLAT_1:35 for T being TopSpace holds Open_Domains_of T c= Domains_of T ; definition let T be TopSpace; func Open_Domains_Union T -> BinOp of (Open_Domains_of T) means :Def10: :: TDLAT_1:def 10 for A, B being Element of Open_Domains_of T holds it . (A,B) = Int (Cl (A \/ B)); existence ex b1 being BinOp of (Open_Domains_of T) st for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B)) proof defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds $2 = Int (Cl (A \/ B)); set D = [:(Open_Domains_of T),(Open_Domains_of T):]; A1: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] ex b being Element of Open_Domains_of T st S1[a,b] proof let a be Element of [:(Open_Domains_of T),(Open_Domains_of T):]; ::_thesis: ex b being Element of Open_Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Open_Domains_of T ; Int (Cl (G \/ F)) is open_condensed by Th23; then Int (Cl (G \/ F)) in { E where E is Subset of T : E is open_condensed } ; then reconsider b = Int (Cl (G \/ F)) as Element of Open_Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Open_Domains_of T; ::_thesis: ( a = [A,B] implies b = Int (Cl (A \/ B)) ) assume a = [A,B] ; ::_thesis: b = Int (Cl (A \/ B)) then A2: [A,B] = [G,F] by MCART_1:21; then A = G by XTUPLE_0:1; hence b = Int (Cl (A \/ B)) by A2, XTUPLE_0:1; ::_thesis: verum end; consider h being Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that A3: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Open_Domains_of T holds h . (A,B) = Int (Cl (A \/ B)) let A, B be Element of Open_Domains_of T; ::_thesis: h . (A,B) = Int (Cl (A \/ B)) thus h . (A,B) = h . [A,B] .= Int (Cl (A \/ B)) by A3 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = Int (Cl (A \/ B)) ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = Int (Cl (A \/ B)) ) holds b1 = b2 proof deffunc H1( Element of Open_Domains_of T, Element of Open_Domains_of T) -> Element of bool the carrier of T = Int (Cl ($1 \/ $2)); thus for o1, o2 being BinOp of (Open_Domains_of T) st ( for a, b being Element of Open_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Open_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def10 defines Open_Domains_Union TDLAT_1:def_10_:_ for T being TopSpace for b2 being BinOp of (Open_Domains_of T) holds ( b2 = Open_Domains_Union T iff for A, B being Element of Open_Domains_of T holds b2 . (A,B) = Int (Cl (A \/ B)) ); notation let T be TopSpace; synonym OPD-Union T for Open_Domains_Union T; end; theorem Th36: :: TDLAT_1:36 for T being TopSpace for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B) proof let T be TopSpace; ::_thesis: for A, B being Element of Open_Domains_of T holds (OPD-Union T) . (A,B) = (D-Union T) . (A,B) let A, B be Element of Open_Domains_of T; ::_thesis: (OPD-Union T) . (A,B) = (D-Union T) . (A,B) A in { D where D is Subset of T : D is open_condensed } ; then consider D being Subset of T such that A1: D = A and A2: D is open_condensed ; A3: A \/ B c= Cl (A \/ B) by PRE_TOPC:18; reconsider A0 = A, B0 = B as Element of Domains_of T ; B in { E where E is Subset of T : E is open_condensed } ; then consider E being Subset of T such that A4: E = B and A5: E is open_condensed ; A6: E is open by A5, TOPS_1:67; D is open by A2, TOPS_1:67; then A7: Int (D \/ E) = D \/ E by A6, TOPS_1:23; thus (OPD-Union T) . (A,B) = Int (Cl (A \/ B)) by Def10 .= (Int (Cl (A0 \/ B0))) \/ (A0 \/ B0) by A1, A4, A7, A3, TOPS_1:19, XBOOLE_1:12 .= (D-Union T) . (A,B) by Def2 ; ::_thesis: verum end; definition let T be TopSpace; func Open_Domains_Meet T -> BinOp of (Open_Domains_of T) means :Def11: :: TDLAT_1:def 11 for A, B being Element of Open_Domains_of T holds it . (A,B) = A /\ B; existence ex b1 being BinOp of (Open_Domains_of T) st for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B proof defpred S1[ set , set ] means for A, B being Element of Open_Domains_of T st $1 = [A,B] holds $2 = A /\ B; set D = [:(Open_Domains_of T),(Open_Domains_of T):]; A1: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] ex b being Element of Open_Domains_of T st S1[a,b] proof let a be Element of [:(Open_Domains_of T),(Open_Domains_of T):]; ::_thesis: ex b being Element of Open_Domains_of T st S1[a,b] reconsider G = a `1 , F = a `2 as Element of Open_Domains_of T ; G in { E where E is Subset of T : E is open_condensed } ; then consider E being Subset of T such that A2: E = G and A3: E is open_condensed ; F in { H where H is Subset of T : H is open_condensed } ; then consider H being Subset of T such that A4: H = F and A5: H is open_condensed ; E /\ H is open_condensed by A3, A5, TOPS_1:69; then G /\ F in { K where K is Subset of T : K is open_condensed } by A2, A4; then reconsider b = G /\ F as Element of Open_Domains_of T ; take b ; ::_thesis: S1[a,b] let A, B be Element of Open_Domains_of T; ::_thesis: ( a = [A,B] implies b = A /\ B ) assume a = [A,B] ; ::_thesis: b = A /\ B then A6: [A,B] = [G,F] by MCART_1:21; then A = G by XTUPLE_0:1; hence b = A /\ B by A6, XTUPLE_0:1; ::_thesis: verum end; consider h being Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Open_Domains_of T) such that A7: for a being Element of [:(Open_Domains_of T),(Open_Domains_of T):] holds S1[a,h . a] from FUNCT_2:sch_3(A1); take h ; ::_thesis: for A, B being Element of Open_Domains_of T holds h . (A,B) = A /\ B let A, B be Element of Open_Domains_of T; ::_thesis: h . (A,B) = A /\ B thus h . (A,B) = h . [A,B] .= A /\ B by A7 ; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (Open_Domains_of T) st ( for A, B being Element of Open_Domains_of T holds b1 . (A,B) = A /\ B ) & ( for A, B being Element of Open_Domains_of T holds b2 . (A,B) = A /\ B ) holds b1 = b2 proof deffunc H1( Element of Open_Domains_of T, Element of Open_Domains_of T) -> Element of bool the carrier of T = $1 /\ $2; thus for o1, o2 being BinOp of (Open_Domains_of T) st ( for a, b being Element of Open_Domains_of T holds o1 . (a,b) = H1(a,b) ) & ( for a, b being Element of Open_Domains_of T holds o2 . (a,b) = H1(a,b) ) holds o1 = o2 from BINOP_2:sch_2(); ::_thesis: verum end; end; :: deftheorem Def11 defines Open_Domains_Meet TDLAT_1:def_11_:_ for T being TopSpace for b2 being BinOp of (Open_Domains_of T) holds ( b2 = Open_Domains_Meet T iff for A, B being Element of Open_Domains_of T holds b2 . (A,B) = A /\ B ); notation let T be TopSpace; synonym OPD-Meet T for Open_Domains_Meet T; end; theorem Th37: :: TDLAT_1:37 for T being TopSpace for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B) proof let T be TopSpace; ::_thesis: for A, B being Element of Open_Domains_of T holds (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B) let A, B be Element of Open_Domains_of T; ::_thesis: (OPD-Meet T) . (A,B) = (D-Meet T) . (A,B) A1: A in { D where D is Subset of T : D is open_condensed } ; reconsider A0 = A, B0 = B as Element of Domains_of T ; B in { E where E is Subset of T : E is open_condensed } ; then consider E being Subset of T such that A2: E = B and A3: E is open_condensed ; consider D being Subset of T such that A4: D = A and A5: D is open_condensed by A1; D /\ E is open_condensed by A5, A3, TOPS_1:69; then A /\ B is condensed by A4, A2, TOPS_1:67; then A6: A /\ B c= Cl (Int (A /\ B)) by TOPS_1:def_6; thus (OPD-Meet T) . (A,B) = A /\ B by Def11 .= (Cl (Int (A0 /\ B0))) /\ (A0 /\ B0) by A6, XBOOLE_1:28 .= (D-Meet T) . (A,B) by Def3 ; ::_thesis: verum end; theorem Th38: :: TDLAT_1:38 for T being TopSpace holds LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice proof 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) #); A1: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-commutative proof let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_4 ::_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; A2: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-absorbing proof let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) "\/" b = b reconsider A = a, B = b as Element of Open_Domains_of T ; B in { D where D is Subset of T : D is open_condensed } ; then A3: ex D being Subset of T st ( D = B & D is open_condensed ) ; a "/\" b = A /\ B by Def11; hence (a "/\" b) "\/" b = Int (Cl ((A /\ B) \/ B)) by Def10 .= Int (Cl B) by XBOOLE_1:22 .= b by A3, TOPS_1:def_8 ; ::_thesis: verum end; A4: 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) #); :: according to LATTICES:def_9 ::_thesis: a "/\" (a "\/" b) = a reconsider A = a, B = b as Element of Open_Domains_of T ; A5: A c= A \/ (Int (Cl B)) by XBOOLE_1:7; 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 A6: A = Int (Cl A) by TOPS_1:def_8; Int ((Cl A) \/ (Cl B)) = Int (Cl (A \/ B)) by PRE_TOPC:20; then A7: A \/ (Int (Cl B)) c= Int (Cl (A \/ B)) by A6, TOPS_1:20; a "\/" b = Int (Cl (A \/ B)) by Def10; hence a "/\" (a "\/" b) = A /\ (Int (Cl (A \/ B))) by Def11 .= a by A5, A7, XBOOLE_1:1, XBOOLE_1:28 ; ::_thesis: verum end; A8: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-associative proof let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_7 ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c reconsider A = a, B = b, C = c as Element of Open_Domains_of T ; A9: a "/\" b = A /\ B by Def11; b "/\" c = B /\ C by Def11; hence a "/\" (b "/\" c) = A /\ (B /\ C) by Def11 .= (A /\ B) /\ C by XBOOLE_1:16 .= (a "/\" b) "/\" c by A9, Def11 ; ::_thesis: verum end; A10: LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is join-associative proof let a, b, c be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_5 ::_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 } ; then A11: ex D being Subset of T st ( D = A & D is open_condensed ) ; B in { E where E is Subset of T : E is open_condensed } ; then A12: ex E being Subset of T st ( E = B & E is open_condensed ) ; C in { F where F is Subset of T : F is open_condensed } ; then A13: ex F being Subset of T st ( F = C & F is open_condensed ) ; A14: a "\/" b = Int (Cl (A \/ B)) by Def10; b "\/" c = Int (Cl (B \/ C)) by Def10; hence a "\/" (b "\/" c) = Int (Cl (A \/ (Int (Cl (B \/ C))))) by Def10 .= Int (Cl ((Int (Cl (A \/ B))) \/ C)) by A11, A12, A13, Th29 .= (a "\/" b) "\/" c by A14, Def10 ; ::_thesis: verum end; LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is meet-commutative proof let a, b be Element of LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #); :: according to LATTICES:def_6 ::_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; then reconsider L = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) as Lattice by A1, A10, A2, A8, A4; A15: L is upper-bounded proof A16: [#] 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 A16, TOPS_1:def_8 ; ::_thesis: a "\/" c = c hence a "\/" c = c ; ::_thesis: verum end; A17: 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 Open_Domains_of T ; A in { D where D is Subset of T : D is open_condensed } ; then consider D being Subset of T such that A18: D = A and A19: D is open_condensed ; A20: D is open by A19, TOPS_1:67; A21: a "/\" c = A /\ C by Def11; C in { F where F is Subset of T : F is open_condensed } ; then consider F being Subset of T such that A22: F = C and F is open_condensed ; B in { E where E is Subset of T : E is open_condensed } ; then consider E being Subset of T such that A23: E = B and E is open_condensed ; A24: a "/\" b = A /\ B by Def11; b "\/" c = Int (Cl (B \/ C)) by Def10; hence a "/\" (b "\/" c) = A /\ (Int (Cl (B \/ C))) by Def11 .= (Int (Cl A)) /\ (Int (Cl (B \/ C))) by A18, A19, TOPS_1:def_8 .= Int (Cl (D /\ (E \/ F))) by A18, A23, A22, A20, Th7 .= Int (Cl ((A /\ B) \/ (A /\ C))) by A18, A23, A22, XBOOLE_1:23 .= (a "/\" b) "\/" (a "/\" c) by A24, A21, Def10 ; ::_thesis: verum end; A25: L is complemented proof [#] 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 ; 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 A26: D = B and A27: D is open_condensed ; A28: D is open by A27, TOPS_1:67; D is condensed by A27, TOPS_1:67; then Int (B `) is open_condensed by A26, 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 A29: B ` misses B by XBOOLE_1:79; A30: 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:15 .= Top L by A30, 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 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 ; 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 Open_Domains_of T ; V in { K where K is Subset of T : K is open_condensed } ; then A32: 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 A32, TOPS_1:def_8 ; ::_thesis: verum end; thus a "/\" b = (Int (B `)) /\ B by Def11 .= (Int (D `)) /\ (Int D) by A26, A28, TOPS_1:23 .= Int ((B `) /\ B) by A26, TOPS_1:17 .= Int ({} T) by A29, XBOOLE_0:def_7 .= Bottom L by A31, LATTICE2:15 ; ::_thesis: b "/\" a = Bottom L hence b "/\" a = Bottom L ; ::_thesis: verum end; L is lower-bounded 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; hence LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) is B_Lattice by A15, A25, A17; ::_thesis: verum end; definition let T be TopSpace; func Open_Domains_Lattice T -> B_Lattice equals :: TDLAT_1:def 12 LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #); coherence LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #) is B_Lattice by Th38; end; :: deftheorem defines Open_Domains_Lattice TDLAT_1:def_12_:_ for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #); begin theorem Th39: :: TDLAT_1:39 for T being TopSpace holds CLD-Union T = (D-Union T) || (Closed_Domains_of T) proof let T be TopSpace; ::_thesis: CLD-Union T = (D-Union T) || (Closed_Domains_of T) reconsider F = CLD-Union T as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) ; reconsider G = (D-Union T) || (Closed_Domains_of T) as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:32; for A, B being Element of Closed_Domains_of T holds F . (A,B) = G . (A,B) proof let A, B be Element of Closed_Domains_of T; ::_thesis: F . (A,B) = G . (A,B) thus F . (A,B) = (D-Union T) . (A,B) by Th32 .= ((D-Union T) || (Closed_Domains_of T)) . [A,B] by FUNCT_1:49 .= G . (A,B) ; ::_thesis: verum end; hence CLD-Union T = (D-Union T) || (Closed_Domains_of T) by BINOP_1:2; ::_thesis: verum end; theorem Th40: :: TDLAT_1:40 for T being TopSpace holds CLD-Meet T = (D-Meet T) || (Closed_Domains_of T) proof let T be TopSpace; ::_thesis: CLD-Meet T = (D-Meet T) || (Closed_Domains_of T) reconsider F = CLD-Meet T as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) ; reconsider G = (D-Meet T) || (Closed_Domains_of T) as Function of [:(Closed_Domains_of T),(Closed_Domains_of T):],(Domains_of T) by FUNCT_2:32; for A, B being Element of Closed_Domains_of T holds F . (A,B) = G . (A,B) proof let A, B be Element of Closed_Domains_of T; ::_thesis: F . (A,B) = G . (A,B) thus F . (A,B) = (D-Meet T) . (A,B) by Th33 .= ((D-Meet T) || (Closed_Domains_of T)) . [A,B] by FUNCT_1:49 .= G . (A,B) ; ::_thesis: verum end; hence CLD-Meet T = (D-Meet T) || (Closed_Domains_of T) by BINOP_1:2; ::_thesis: verum end; theorem :: TDLAT_1:41 for T being TopSpace holds Closed_Domains_Lattice T is SubLattice of Domains_Lattice T proof let T be TopSpace; ::_thesis: Closed_Domains_Lattice T is SubLattice of Domains_Lattice T set L = Domains_Lattice T; set CL = Closed_Domains_Lattice T; thus the carrier of (Closed_Domains_Lattice T) c= the carrier of (Domains_Lattice T) ; :: according to NAT_LAT:def_12 ::_thesis: ( the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) & the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) ) thus the L_join of (Closed_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th39; ::_thesis: the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) thus the L_meet of (Closed_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Closed_Domains_Lattice T) by Th40; ::_thesis: verum end; theorem Th42: :: TDLAT_1:42 for T being TopSpace holds OPD-Union T = (D-Union T) || (Open_Domains_of T) proof let T be TopSpace; ::_thesis: OPD-Union T = (D-Union T) || (Open_Domains_of T) reconsider F = OPD-Union T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) ; reconsider G = (D-Union T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:32; for A, B being Element of Open_Domains_of T holds F . (A,B) = G . (A,B) proof let A, B be Element of Open_Domains_of T; ::_thesis: F . (A,B) = G . (A,B) thus F . (A,B) = (D-Union T) . (A,B) by Th36 .= ((D-Union T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:49 .= G . (A,B) ; ::_thesis: verum end; hence OPD-Union T = (D-Union T) || (Open_Domains_of T) by BINOP_1:2; ::_thesis: verum end; theorem Th43: :: TDLAT_1:43 for T being TopSpace holds OPD-Meet T = (D-Meet T) || (Open_Domains_of T) proof let T be TopSpace; ::_thesis: OPD-Meet T = (D-Meet T) || (Open_Domains_of T) reconsider F = OPD-Meet T as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) ; reconsider G = (D-Meet T) || (Open_Domains_of T) as Function of [:(Open_Domains_of T),(Open_Domains_of T):],(Domains_of T) by FUNCT_2:32; for A, B being Element of Open_Domains_of T holds F . (A,B) = G . (A,B) proof let A, B be Element of Open_Domains_of T; ::_thesis: F . (A,B) = G . (A,B) thus F . (A,B) = (D-Meet T) . (A,B) by Th37 .= ((D-Meet T) || (Open_Domains_of T)) . [A,B] by FUNCT_1:49 .= G . (A,B) ; ::_thesis: verum end; hence OPD-Meet T = (D-Meet T) || (Open_Domains_of T) by BINOP_1:2; ::_thesis: verum end; theorem :: TDLAT_1:44 for T being TopSpace holds Open_Domains_Lattice T is SubLattice of Domains_Lattice T proof let T be TopSpace; ::_thesis: Open_Domains_Lattice T is SubLattice of Domains_Lattice T set L = Domains_Lattice T; set OL = Open_Domains_Lattice T; thus the carrier of (Open_Domains_Lattice T) c= the carrier of (Domains_Lattice T) ; :: according to NAT_LAT:def_12 ::_thesis: ( the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) & the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) ) thus the L_join of (Open_Domains_Lattice T) = the L_join of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th42; ::_thesis: the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) thus the L_meet of (Open_Domains_Lattice T) = the L_meet of (Domains_Lattice T) || the carrier of (Open_Domains_Lattice T) by Th43; ::_thesis: verum end;