let FT be non empty RelStr ; :: thesis: for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
let A be Subset of FT; :: thesis: ( A ^s <> {} & card A <> 1 implies not A is connected )
assume A1: ( A ^s <> {} & card A <> 1 ) ; :: thesis: not A is connected
then consider z being Element of FT such that
A2: z in A ^s by SUBSET_1:10;
A3: ( z in A & (U_FT z) \ {z} misses A ) by A2, Th14;
set B = A \ {z};
set C = {z};
{z} is Subset of A by A3, SUBSET_1:63;
then A4: A = (A \ {z}) \/ {z} by XBOOLE_1:45;
A5: card {z} = 1 by CARD_1:50;
A <> {} by A2, Th14;
then A6: A \ {z} <> {} by A1, A5, ZFMISC_1:66;
A7: A \ {z} misses {z} by XBOOLE_1:79;
(A \ {z}) ^b misses {z}

proof

assume (A \ {z}) ^b meets {z} ; :: thesis: contradiction
then consider x being set such that
A8: ( x in (A \ {z}) ^b & x in {z} ) by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
U_FT x meets A \ {z} by A8, Th13;
then consider y being set such that
A9: ( y in U_FT x & y in A \ {z} ) by XBOOLE_0:3;
A10: x = z by A8, TARSKI:def 1;
not x in A \ {z} by A8, XBOOLE_0:def 5;
then y in (U_FT x) \ {x} by A9, ZFMISC_1:64;
then (U_FT z) \ {z} meets A \ {z} by A9, A10, XBOOLE_0:3;
then consider w being set such that
A11: w in ((U_FT z) \ {z}) /\ (A \ {z}) by XBOOLE_0:4;
((U_FT z) \ {z}) /\ (A \ {z}) c= ((U_FT z) \ {z}) /\ A by XBOOLE_1:26, XBOOLE_1:36;
hence contradiction by A3, A11, XBOOLE_0:4; :: thesis: verum

end;

hence not A is connected by A4, A6, A7, Def18; :: thesis: verum