let TS be TopStruct ; :: thesis: for K, L, K1, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated
let K, L, K1, L1 be Subset of TS; :: thesis: ( K,L are_separated & K1 c= K & L1 c= L implies K1,L1 are_separated )
assume that
A1: ( (Cl K) /\ L = {} & K /\ (Cl L) = {} ) and
A2: K1 c= K and
A3: L1 c= L ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: K1,L1 are_separated
( Cl K1 c= Cl K & Cl L1 c= Cl L ) by A2, A3, PRE_TOPC:49;
then ( (Cl K1) /\ L1 = {} TS & K1 /\ (Cl L1) = {} TS ) by A1, A2, A3, XBOOLE_1:3, XBOOLE_1:27;
then ( Cl K1 misses L1 & K1 misses Cl L1 ) by XBOOLE_0:def 7;
hence K1,L1 are_separated by Def1; :: thesis: verum