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: ((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 ;
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:20 ;
hence Fr (A /\ B) c= ((Cl A) /\ (Fr B)) \/ ((Fr A) /\ (Cl B)) by A1, PRE_TOPC:21, XBOOLE_1:26; :: thesis: verum