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;
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))
per cases ( 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)) ;
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)) ;
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; :: thesis: verum