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) \/ (Cl L)) /\ (Cl ((K \/ L) `)) by PRE_TOPC:20
.= (Cl ((K `) /\ (L `))) /\ ((Cl K) \/ (Cl L)) by XBOOLE_1:53
.= ((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