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_separated iff B1,B2 are_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_separated iff B1,B2 are_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_separated iff B1,B2 are_separated )

let B1, B2 be Subset of X0; :: thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_separated iff B1,B2 are_separated ) )

assume that

A1: B1 = A1 and

A2: B2 = A2 ; :: thesis: ( A1,A2 are_separated iff B1,B2 are_separated )

A3: Cl B2 = (Cl A2) /\ ([#] X0) by A2, PRE_TOPC:17;

A4: Cl B1 = (Cl A1) /\ ([#] X0) by A1, PRE_TOPC:17;

thus ( A1,A2 are_separated implies B1,B2 are_separated ) :: thesis: ( B1,B2 are_separated implies A1,A2 are_separated )

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds

( A1,A2 are_separated iff B1,B2 are_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_separated iff B1,B2 are_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_separated iff B1,B2 are_separated )

let B1, B2 be Subset of X0; :: thesis: ( B1 = A1 & B2 = A2 implies ( A1,A2 are_separated iff B1,B2 are_separated ) )

assume that

A1: B1 = A1 and

A2: B2 = A2 ; :: thesis: ( A1,A2 are_separated iff B1,B2 are_separated )

A3: Cl B2 = (Cl A2) /\ ([#] X0) by A2, PRE_TOPC:17;

A4: Cl B1 = (Cl A1) /\ ([#] X0) by A1, PRE_TOPC:17;

thus ( A1,A2 are_separated implies B1,B2 are_separated ) :: thesis: ( B1,B2 are_separated implies A1,A2 are_separated )

proof

thus
( B1,B2 are_separated implies A1,A2 are_separated )
:: thesis: verum
assume A5:
A1,A2 are_separated
; :: thesis: B1,B2 are_separated

then A1 misses Cl A2 by CONNSP_1:def 1;

then A1 /\ (Cl A2) = {} ;

then B1 /\ (Cl B2) = {} /\ ([#] X0) by A1, A3, XBOOLE_1:16;

then A6: B1 misses Cl B2 ;

Cl A1 misses A2 by A5, CONNSP_1:def 1;

then (Cl A1) /\ A2 = {} ;

then (Cl B1) /\ B2 = {} /\ ([#] X0) by A2, A4, XBOOLE_1:16;

then Cl B1 misses B2 ;

hence B1,B2 are_separated by A6, CONNSP_1:def 1; :: thesis: verum

end;then A1 misses Cl A2 by CONNSP_1:def 1;

then A1 /\ (Cl A2) = {} ;

then B1 /\ (Cl B2) = {} /\ ([#] X0) by A1, A3, XBOOLE_1:16;

then A6: B1 misses Cl B2 ;

Cl A1 misses A2 by A5, CONNSP_1:def 1;

then (Cl A1) /\ A2 = {} ;

then (Cl B1) /\ B2 = {} /\ ([#] X0) by A2, A4, XBOOLE_1:16;

then Cl B1 misses B2 ;

hence B1,B2 are_separated by A6, CONNSP_1:def 1; :: thesis: verum

proof

assume A7:
B1,B2 are_separated
; :: thesis: A1,A2 are_separated

then (Cl A1) /\ ([#] X0) misses A2 by A2, A4, CONNSP_1:def 1;

then ((Cl A1) /\ ([#] X0)) /\ A2 = {} ;

then A8: ((Cl A1) /\ A2) /\ ([#] X0) = {} by XBOOLE_1:16;

A1 misses (Cl A2) /\ ([#] X0) by A1, A3, A7, CONNSP_1:def 1;

then A1 /\ ((Cl A2) /\ ([#] X0)) = {} ;

then A9: (A1 /\ (Cl A2)) /\ ([#] X0) = {} by XBOOLE_1:16;

A1 /\ (Cl A2) c= A1 by XBOOLE_1:17;

then A1 /\ (Cl A2) = {} by A1, A9, XBOOLE_1:1, XBOOLE_1:28;

then A10: A1 misses Cl A2 ;

(Cl A1) /\ A2 c= A2 by XBOOLE_1:17;

then (Cl A1) /\ A2 = {} by A2, A8, XBOOLE_1:1, XBOOLE_1:28;

then Cl A1 misses A2 ;

hence A1,A2 are_separated by A10, CONNSP_1:def 1; :: thesis: verum

end;then (Cl A1) /\ ([#] X0) misses A2 by A2, A4, CONNSP_1:def 1;

then ((Cl A1) /\ ([#] X0)) /\ A2 = {} ;

then A8: ((Cl A1) /\ A2) /\ ([#] X0) = {} by XBOOLE_1:16;

A1 misses (Cl A2) /\ ([#] X0) by A1, A3, A7, CONNSP_1:def 1;

then A1 /\ ((Cl A2) /\ ([#] X0)) = {} ;

then A9: (A1 /\ (Cl A2)) /\ ([#] X0) = {} by XBOOLE_1:16;

A1 /\ (Cl A2) c= A1 by XBOOLE_1:17;

then A1 /\ (Cl A2) = {} by A1, A9, XBOOLE_1:1, XBOOLE_1:28;

then A10: A1 misses Cl A2 ;

(Cl A1) /\ A2 c= A2 by XBOOLE_1:17;

then (Cl A1) /\ A2 = {} by A2, A8, XBOOLE_1:1, XBOOLE_1:28;

then Cl A1 misses A2 ;

hence A1,A2 are_separated by A10, CONNSP_1:def 1; :: thesis: verum