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 that
A1: A ^s <> {} and
A2: card A <> 1 ; :: thesis: not A is connected
consider z being Element of FT such that
A3: z in A ^s by A1, SUBSET_1:4;
set C = {z};
set B = A \ {z};
( card {z} = 1 & A <> {} ) by A3, Th9, CARD_1:30;
then A4: A \ {z} <> {} by A2, ZFMISC_1:58;
z in A by A3, Th9;
then {z} is Subset of A by SUBSET_1:41;
then A5: A = (A \ {z}) \/ {z} by XBOOLE_1:45;
A6: (U_FT z) \ {z} misses A by A3, Th9;
A7: (A \ {z}) ^b misses {z}

proof

assume (A \ {z}) ^b meets {z} ; :: thesis: contradiction
then consider x being object such that
A8: x in (A \ {z}) ^b and
A9: x in {z} by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
A10: x = z by A9, TARSKI:def 1;
U_FT x meets A \ {z} by A8, Th8;
then consider y being object such that
A11: y in U_FT x and
A12: y in A \ {z} by XBOOLE_0:3;
not x in A \ {z} by A9, XBOOLE_0:def 5;
then y in (U_FT x) \ {x} by A11, A12, ZFMISC_1:56;
then (U_FT z) \ {z} meets A \ {z} by A12, A10, XBOOLE_0:3;
then A13: ex w being object st 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 A6, A13; :: thesis: verum

end;

A \ {z} misses {z} by XBOOLE_1:79;
hence not A is connected by A5, A4, A7; :: thesis: verum