let FT be non empty RelStr ; :: thesis: for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds

A1,B1 are_separated

let A, B, A1, B1 be Subset of FT; :: thesis: ( A,B are_separated & A1 c= A & B1 c= B implies A1,B1 are_separated )

assume that

A1: A,B are_separated and

A2: A1 c= A and

A3: B1 c= B ; :: thesis: A1,B1 are_separated

A misses B ^b by A1, FINTOPO4:def 1;

then A4: A /\ (B ^b) = {} ;

B1 ^b c= B ^b by A3, FIN_TOPO:14;

then A1 /\ (B1 ^b) = {} FT by A2, A4, XBOOLE_1:3, XBOOLE_1:27;

then A5: A1 misses B1 ^b ;

A ^b misses B by A1, FINTOPO4:def 1;

then A6: (A ^b) /\ B = {} ;

A1 ^b c= A ^b by A2, FIN_TOPO:14;

then (A1 ^b) /\ B1 = {} FT by A3, A6, XBOOLE_1:3, XBOOLE_1:27;

then A1 ^b misses B1 ;

hence A1,B1 are_separated by A5, FINTOPO4:def 1; :: thesis: verum

A1,B1 are_separated

let A, B, A1, B1 be Subset of FT; :: thesis: ( A,B are_separated & A1 c= A & B1 c= B implies A1,B1 are_separated )

assume that

A1: A,B are_separated and

A2: A1 c= A and

A3: B1 c= B ; :: thesis: A1,B1 are_separated

A misses B ^b by A1, FINTOPO4:def 1;

then A4: A /\ (B ^b) = {} ;

B1 ^b c= B ^b by A3, FIN_TOPO:14;

then A1 /\ (B1 ^b) = {} FT by A2, A4, XBOOLE_1:3, XBOOLE_1:27;

then A5: A1 misses B1 ^b ;

A ^b misses B by A1, FINTOPO4:def 1;

then A6: (A ^b) /\ B = {} ;

A1 ^b c= A ^b by A2, FIN_TOPO:14;

then (A1 ^b) /\ B1 = {} FT by A3, A6, XBOOLE_1:3, XBOOLE_1:27;

then A1 ^b misses B1 ;

hence A1,B1 are_separated by A5, FINTOPO4:def 1; :: thesis: verum