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

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

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

then A3: A8 = {} FT ;
B8 = {} X' by A1, A2;
hence ( A8 is connected iff B8 is connected ) by A3; :: thesis: verum

end;

suppose A4: 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 X' by A1, A4;
reconsider X = X' as non empty RelStr ;

A5: now

assume not A8 is connected ; :: thesis: not B8 is connected
then consider P, Q being Subset of FT such that
A6: A8 = P \/ Q and
A7: P <> {} and
A8: Q <> {} and
A9: P misses Q and
A10: P ^b misses Q by FIN_TOPO:def 18;
P c= A8 by A6, XBOOLE_1:7;
then reconsider P' = P as Subset of X by A1, XBOOLE_1:1;
Q c= A8 by A6, XBOOLE_1:7;
then reconsider Q' = Q as Subset of X by A1, XBOOLE_1:1;
A11: P' ^b = (P ^b ) /\ ([#] X) by Th13;
A12: Q' c= the carrier of X ;
(P' ^b ) /\ Q' = (P ^b ) /\ (([#] X) /\ Q) by A11, XBOOLE_1:16
.= (P ^b ) /\ Q by A12, XBOOLE_1:28
.= {} by A10, XBOOLE_0:def 7 ;
then P' ^b misses Q' by XBOOLE_0:def 7;
hence not B8 is connected by A1, A6, A7, A8, A9, 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 X' such that
A13: B8 = P \/ Q and
A14: P <> {} and
A15: Q <> {} and
A16: P misses Q and
A17: P ^b misses Q by FIN_TOPO:def 18;
the carrier of X c= the carrier of FT by Def2;
then reconsider P' = P as Subset of FT by XBOOLE_1:1;
the carrier of X c= the carrier of FT by Def2;
then reconsider Q' = Q as Subset of FT by XBOOLE_1:1;
A18: P ^b = (P' ^b ) /\ ([#] X) by Th13;
(P' ^b ) /\ Q' = (P' ^b ) /\ (([#] X) /\ Q) by XBOOLE_1:28
.= (P ^b ) /\ Q by A18, XBOOLE_1:16
.= {} by A17, XBOOLE_0:def 7 ;
then P' ^b misses Q' by XBOOLE_0:def 7;
hence not A is connected by A1, A13, A14, A15, A16, FIN_TOPO:def 18; :: thesis: verum

end;

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

end;

end;