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 ^b misses B & A misses B ^b ) by A1, FINTOPO4:def 1;
then A4: ( (A ^b ) /\ B = {} & A /\ (B ^b ) = {} ) by XBOOLE_0:def 7;
( A1 ^b c= A ^b & B1 ^b c= B ^b ) by A2, A3, FIN_TOPO:19;
then ( (A1 ^b ) /\ B1 = {} FT & A1 /\ (B1 ^b ) = {} FT ) by A2, A3, A4, XBOOLE_1:3, XBOOLE_1:27;
then ( A1 ^b misses B1 & A1 misses B1 ^b ) by XBOOLE_0:def 7;
hence A1,B1 are_separated by FINTOPO4:def 1; :: thesis: verum