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