let FT be non empty RelStr ; for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
let A be Subset of FT; ( A ^s <> {} & card A <> 1 implies not A is connected )
assume that
A1:
A ^s <> {}
and
A2:
card A <> 1
; 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, Th14, CARD_1:30;
then A4:
A \ {z} <> {}
by A2, ZFMISC_1:58;
z in A
by A3, Th14;
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, Th14;
A7:
(A \ {z}) ^b misses {z}
proof
assume
(A \ {z}) ^b meets {z}
;
contradiction
then consider x being
set 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, Th13;
then consider y being
set 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
set 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, XBOOLE_0:4;
verum
end;
A \ {z} misses {z}
by XBOOLE_1:79;
hence
not A is connected
by A5, A4, A7, Def18; verum