let FT be non empty RelStr ; :: thesis: for X' being non empty SubSpace of FT
for A being Subset of
for B being Subset of st A = B holds
( A is connected iff B is connected )
let X' be non empty SubSpace of FT; :: thesis: for A being Subset of
for B being Subset of st A = B holds
( A is connected iff B is connected )
let A8 be Subset of ; :: thesis: for B being Subset of st A8 = B holds
( A8 is connected iff B is connected )
let B8 be Subset of ; :: 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 ;
reconsider B = B8 as non empty Subset of by A1, A2;
reconsider X = X' as non empty RelStr ;

A3: now

assume not A8 is connected ; :: thesis: not B8 is connected
then consider P, Q being Subset of 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 Q' = Q as Subset of by A1, XBOOLE_1:1;
P c= A8 by A4, XBOOLE_1:7;
then reconsider P' = P as Subset of by A1, XBOOLE_1:1;
A7: Q' c= the carrier of X ;
P' ^b = (P ^b ) /\ ([#] X) by Th13;
then (P' ^b ) /\ Q' = (P ^b ) /\ (([#] X) /\ Q) by XBOOLE_1:16
.= (P ^b ) /\ Q by A7, XBOOLE_1:28
.= {} by A6, XBOOLE_0:def 7 ;
then P' ^b misses Q' 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 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 Q' = Q as Subset of by XBOOLE_1:1;
the carrier of X c= the carrier of FT by Def2;
then reconsider P' = P as Subset of by XBOOLE_1:1;
A10: P ^b = (P' ^b ) /\ ([#] X) by Th13;
(P' ^b ) /\ Q' = (P' ^b ) /\ (([#] X) /\ Q) by XBOOLE_1:28
.= (P ^b ) /\ Q by A10, XBOOLE_1:16
.= {} by A9, XBOOLE_0:def 7 ;
then P' ^b misses Q' 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;