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;
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;
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