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:49, 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:49, 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:50
.= ((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