let FT be non empty RelStr ; :: thesis: for A being non empty Subset of FT holds
( A is connected iff FT | A is connected )
let A be non empty Subset of FT; :: thesis: ( A is connected iff FT | A is connected )
A1: [#] (FT | A) = A by Def3;
thus ( A is connected implies FT | A is connected ) :: thesis: ( FT | A is connected implies A is connected )

proof

assume A2: A is connected ; :: thesis: FT | A is connected
for B2, C2 being Subset of (FT | A) st [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds
B2 ^b meets C2

proof

let B2, C2 be Subset of (FT | A); :: thesis: ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 )
A3: ([#] (FT | A)) /\ C2 = C2 by XBOOLE_1:28;
the carrier of (FT | A) = [#] (FT | A)
.= A by Def3 ;
then reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1:1;
assume ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 ) ; :: thesis: B2 ^b meets C2
then A4: B3 ^b meets C3 by A1, A2;
(B2 ^b) /\ C2 = ((B3 ^b) /\ ([#] (FT | A))) /\ C2 by Th12
.= (B3 ^b) /\ C3 by A3, XBOOLE_1:16 ;
then (B2 ^b) /\ C2 <> {} by A4;
hence B2 ^b meets C2 ; :: thesis: verum

end;

then [#] (FT | A) is connected ;
hence FT | A is connected ; :: thesis: verum

end;

assume FT | A is connected ; :: thesis: A is connected
then A5: [#] (FT | A) is connected ;
let B, C be Subset of FT; :: according to FIN_TOPO:def 16 :: thesis: ( not A = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )
assume that
A6: A = B \/ C and
A7: ( B <> {} & C <> {} & B misses C ) ; :: thesis: not B ^b misses C
A8: [#] (FT | A) = A by Def3;
then reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1:7;
reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1:7;
( ([#] (FT | A)) /\ C2 = C2 & B2 ^b = (B ^b) /\ ([#] (FT | A)) ) by Th12, XBOOLE_1:28;
then A9: (B ^b) /\ C = (B2 ^b) /\ C2 by XBOOLE_1:16;
B2 ^b meets C2 by A5, A6, A7, A8;
hence (B ^b) /\ C <> {} by A9; :: according to XBOOLE_0:def 7 :: thesis: verum