let FT be non empty RelStr ; :: thesis: for X9 being non empty SubSpace of FT
for A being Subset of FT
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let X9 be non empty SubSpace of FT; :: thesis: for A being Subset of FT
for B being Subset of X9 st A = B holds
( A is connected iff B is connected )
let A8 be Subset of FT; :: thesis: for B being Subset of X9 st A8 = B holds
( A8 is connected iff B is connected )
let B8 be Subset of X9; :: thesis: ( A8 = B8 implies ( A8 is connected iff B8 is connected ) )
assume A1: A8 = B8 ; :: thesis: ( A8 is connected iff B8 is connected )

per cases ( A8 = {} or A8 <> {} ) ;

suppose A8 = {} ; :: thesis: ( A8 is connected iff B8 is connected )

hence ( A8 is connected iff B8 is connected ) by A1; :: thesis: verum

end;

suppose A2: A8 <> {} ; :: thesis: ( A8 is connected iff B8 is connected )

then reconsider A = A8 as non empty Subset of FT ;
reconsider B = B8 as non empty Subset of X9 by A1, A2;
reconsider X = X9 as non empty RelStr ;

A3: now

assume not A8 is connected ; :: thesis: not B8 is connected
then consider P, Q being Subset of FT such that
A4: A8 = P \/ Q and
A5: ( P <> {} & Q <> {} & P misses Q ) and
A6: P ^b misses Q by FIN_TOPO:def 18;
Q c= A8 by A4, XBOOLE_1:7;
then reconsider Q9 = Q as Subset of X by A1, XBOOLE_1:1;
P c= A8 by A4, XBOOLE_1:7;
then reconsider P9 = P as Subset of X by A1, XBOOLE_1:1;
A7: Q9 c= the carrier of X ;
P9 ^b = (P ^b) /\ ([#] X) by Th13;
then (P9 ^b) /\ Q9 = (P ^b) /\ (([#] X) /\ Q) by XBOOLE_1:16
.= (P ^b) /\ Q by A7, XBOOLE_1:28
.= {} by A6, XBOOLE_0:def 7 ;
then P9 ^b misses Q9 by XBOOLE_0:def 7;
hence not B8 is connected by A1, A4, A5, FIN_TOPO:def 18; :: thesis: verum

end;

now

assume not B is connected ; :: thesis: not A is connected
then consider P, Q being Subset of X9 such that
A8: ( B8 = P \/ Q & P <> {} & Q <> {} & P misses Q ) and
A9: P ^b misses Q by FIN_TOPO:def 18;
the carrier of X c= the carrier of FT by Def2;
then reconsider Q9 = Q as Subset of FT by XBOOLE_1:1;
the carrier of X c= the carrier of FT by Def2;
then reconsider P9 = P as Subset of FT by XBOOLE_1:1;
A10: P ^b = (P9 ^b) /\ ([#] X) by Th13;
(P9 ^b) /\ Q9 = (P9 ^b) /\ (([#] X) /\ Q) by XBOOLE_1:28
.= (P ^b) /\ Q by A10, XBOOLE_1:16
.= {} by A9, XBOOLE_0:def 7 ;
then P9 ^b misses Q9 by XBOOLE_0:def 7;
hence not A is connected by A1, A8, FIN_TOPO:def 18; :: thesis: verum

end;

hence ( A8 is connected iff B8 is connected ) by A3; :: thesis: verum

end;

end;