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}

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

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

A \ {z} misses {z}
by XBOOLE_1:79;
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;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

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