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:48, XBOOLE_1:9;
(A \/ B) \/ ((A \/ B) ` ) = [#] T by PRE_TOPC:18;
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:49;
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:49;
assume A5: ( A is closed or B is closed ) ; :: thesis: (Cl (Int A)) \/ (Cl (Int B)) = Cl (Int (A \/ B))

A6: now

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:52;
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:49;
then Cl (A ` ) c= (Cl (Int B)) \/ (Cl (Cl ((B \/ A) ` ))) by PRE_TOPC:50;
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:18;
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:49;
then Cl (Int (B \/ A)) c= (Cl (Cl (Int B))) \/ (Cl (Int A)) by PRE_TOPC:50;
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:52;
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:49;
then Cl (B ` ) c= (Cl (Int A)) \/ (Cl (Cl ((A \/ B) ` ))) by PRE_TOPC:50;
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:18;
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:49;
then Cl (Int (A \/ B)) c= (Cl (Cl (Int A))) \/ (Cl (Int B)) by PRE_TOPC:50;
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:48, XBOOLE_1:7;
then A7: Cl (Int B) c= Cl (Int (A \/ B)) by PRE_TOPC:49;
Int A c= Int (A \/ B) by TOPS_1:48, XBOOLE_1:7;
then Cl (Int A) c= Cl (Int (A \/ B)) by PRE_TOPC:49;
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