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