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

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