let T be TopSpace; :: thesis: for A, B being Subset of T holds Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))
let A, B be Subset of T; :: thesis: Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B))
A1: Fr (A /\ B) = (Cl (A /\ B)) /\ (Cl ((A /\ B) ` )) by TOPS_1:def 2
.= (Cl (A /\ B)) /\ (Cl ((A ` ) \/ (B ` ))) by XBOOLE_1:54
.= (Cl (A /\ B)) /\ ((Cl (A ` )) \/ (Cl (B ` ))) by PRE_TOPC:50 ;
((Cl A) /\ (Cl B)) /\ ((Cl (A ` )) \/ (Cl (B ` ))) = (((Cl A) /\ (Cl B)) /\ (Cl (A ` ))) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B ` ))) by XBOOLE_1:23
.= (((Cl A) /\ (Cl (A ` ))) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B ` ))) by XBOOLE_1:16
.= ((Fr A) /\ (Cl B)) \/ (((Cl A) /\ (Cl B)) /\ (Cl (B ` ))) by TOPS_1:def 2
.= ((Fr A) /\ (Cl B)) \/ ((Cl A) /\ ((Cl B) /\ (Cl (B ` )))) by XBOOLE_1:16
.= ((Fr A) /\ (Cl B)) \/ ((Cl A) /\ (Fr B)) by TOPS_1:def 2 ;
hence Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B)) by A1, PRE_TOPC:51, XBOOLE_1:26; :: thesis: verum