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 ;
set C = {z};
set B = A \ {z};
( card {z} = 1 & A <> {} ) by ;
then A4: A \ {z} <> {} by ;
z in A by ;
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 ;
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 ;
U_FT x meets A \ {z} by ;
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 ;
then y in (U_FT x) \ {x} by ;
then (U_FT z) \ {z} meets A \ {z} by ;
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 ;
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