let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X
for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let A1, A2 be Subset of X; :: thesis: for X0 being non empty SubSpace of X
for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let X0 be non empty SubSpace of X; :: thesis: for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds
( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
let B1, B2 be Subset of X0; :: thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated ) )
assume A1: ( B1 = A1 & B2 = A2 ) ; :: thesis: ( A1,A2 are_weakly_separated iff B1,B2 are_weakly_separated )
thus ( A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated ) :: thesis: ( B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated )

proof

assume A1,A2 are_weakly_separated ; :: thesis: B1,B2 are_weakly_separated
then A1 \ A2,A2 \ A1 are_separated by TSEP_1:def 5;
then B1 \ B2,B2 \ B1 are_separated by A1, Th26;
hence B1,B2 are_weakly_separated by TSEP_1:def 5; :: thesis: verum

end;

thus ( B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated ) :: thesis: verum

proof

assume B1,B2 are_weakly_separated ; :: thesis: A1,A2 are_weakly_separated
then B1 \ B2,B2 \ B1 are_separated by TSEP_1:def 5;
then A1 \ A2,A2 \ A1 are_separated by A1, Th26;
hence A1,A2 are_weakly_separated by TSEP_1:def 5; :: thesis: verum

end;