let TS be TopSpace; :: thesis: for K, L being Subset of TS holds Fr (K /\ L) c= (Fr K) \/ (Fr L)
let K, L be Subset of TS; :: thesis: Fr (K /\ L) c= (Fr K) \/ (Fr L)
Cl (K /\ L) c= Cl K by PRE_TOPC:19, XBOOLE_1:17;
then A1: (Cl (K /\ L)) /\ (Cl (K `)) c= (Cl K) /\ (Cl (K `)) by XBOOLE_1:26;
Cl (K /\ L) c= Cl L by PRE_TOPC:19, XBOOLE_1:17;
then A2: (Cl (K /\ L)) /\ (Cl (L `)) c= (Cl L) /\ (Cl (L `)) by XBOOLE_1:26;
Fr (K /\ L) = (Cl (K /\ L)) /\ (Cl ((K `) \/ (L `))) by XBOOLE_1:54
.= (Cl (K /\ L)) /\ ((Cl (K `)) \/ (Cl (L `))) by PRE_TOPC:20
.= ((Cl (K /\ L)) /\ (Cl (K `))) \/ ((Cl (K /\ L)) /\ (Cl (L `))) by XBOOLE_1:23 ;
hence Fr (K /\ L) c= (Fr K) \/ (Fr L) by A1, A2, XBOOLE_1:13; :: thesis: verum