let TS be TopStruct ; :: thesis: for K, K1, L, L1 being Subset of TS st K,L are_separated & K1 c= K & L1 c= L holds
K1,L1 are_separated
let K, K1, L, 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 = {} and
A2: K /\ (Cl L) = {} and
A3: K1 c= K and
A4: L1 c= L ; :: according to XBOOLE_0:def 7,CONNSP_1:def 1 :: thesis: K1,L1 are_separated
Cl L1 c= Cl L by A4, PRE_TOPC:19;
then K1 /\ (Cl L1) = {} TS by A2, A3, XBOOLE_1:3, XBOOLE_1:27;
then A5: K1 misses Cl L1 ;
Cl K1 c= Cl K by A3, PRE_TOPC:19;
then (Cl K1) /\ L1 = {} TS by A1, A4, XBOOLE_1:3, XBOOLE_1:27;
then Cl K1 misses L1 ;
hence K1,L1 are_separated by A5; :: thesis: verum