let FT be non empty RelStr ; :: thesis: for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds
A is connected
let A, C be Subset of FT; :: thesis: ( FT is symmetric & C is connected & C c= A & A c= C ^b implies A is connected )
assume that
A1: FT is symmetric and
A2: C is connected and
A3: C c= A and
A4: A c= C ^b ; :: thesis: A is connected
let P2, Q2 be Subset of FT; :: according to FIN_TOPO:def 18 :: thesis: ( not A = P2 \/ Q2 or P2 = {} or Q2 = {} or not P2 misses Q2 or not P2 ^b misses Q2 )
assume that
A5: A = P2 \/ Q2 and
A6: P2 <> {} and
A7: Q2 <> {} and
A8: P2 misses Q2 ; :: thesis: not P2 ^b misses Q2
assume A9: P2 ^b misses Q2 ; :: thesis: contradiction
consider x2 being Element of Q2;
A10: x2 in Q2 by A7;
Q2 c= Q2 \/ P2 by XBOOLE_1:7;
then Q2 c= C ^b by A4, A5, XBOOLE_1:1;
then x2 in C ^b by A10;
then consider z2 being Element of FT such that
A11: z2 = x2 and
A12: U_FT z2 meets C ;
consider y3 being Element of (U_FT z2) /\ C;
A13: (U_FT z2) /\ C <> {} by A12, XBOOLE_0:def 7;
then y3 in (U_FT z2) /\ C ;
then reconsider y4 = y3 as Element of FT ;
y3 in U_FT z2 by A13, XBOOLE_0:def 4;
then z2 in U_FT y4 by A1, FIN_TOPO:def 15;
then z2 in (U_FT y4) /\ Q2 by A7, A11, XBOOLE_0:def 4;
then A14: U_FT y4 meets Q2 by XBOOLE_0:def 7;
set P3 = P2 /\ C;
set Q3 = Q2 /\ C;
A15: C = A /\ C by A3, XBOOLE_1:28
.= (P2 /\ C) \/ (Q2 /\ C) by A5, XBOOLE_1:23 ;
consider x being Element of P2;
A16: x in P2 by A6;
P2 c= P2 \/ Q2 by XBOOLE_1:7;
then P2 c= C ^b by A4, A5, XBOOLE_1:1;
then x in C ^b by A16;
then consider z being Element of FT such that
A17: z = x and
A18: U_FT z meets C ;
consider y being Element of (U_FT z) /\ C;
A19: (U_FT z) /\ C <> {} by A18, XBOOLE_0:def 7;
then y in (U_FT z) /\ C ;
then reconsider y2 = y as Element of FT ;
y in U_FT z by A19, XBOOLE_0:def 4;
then z in U_FT y2 by A1, FIN_TOPO:def 15;
then z in (U_FT y2) /\ P2 by A6, A17, XBOOLE_0:def 4;
then U_FT y2 meets P2 by XBOOLE_0:def 7;
then A20: y2 in P2 ^b ;
A21: y4 in C by A13, XBOOLE_0:def 4;

A22: now

assume Q2 /\ C = {} ; :: thesis: contradiction
then A23: y4 in P2 by A21, A15, XBOOLE_0:def 4;
consider w being Element of FT such that
A24: w = y4 and
A25: U_FT w meets Q2 by A14;
consider s being set such that
A26: s in U_FT w and
A27: s in Q2 by A25, XBOOLE_0:3;
reconsider s2 = s as Element of FT by A26;
w in U_FT s2 by A1, A26, FIN_TOPO:def 15;
then U_FT s2 meets P2 by A23, A24, XBOOLE_0:3;
then s2 in P2 ^b ;
hence contradiction by A9, A27, XBOOLE_0:3; :: thesis: verum

end;

A28: P2 /\ C c= P2 by XBOOLE_1:17;
A29: y2 in C by A19, XBOOLE_0:def 4;

A30: now

assume P2 /\ C = {} ; :: thesis: contradiction
then y2 in Q2 by A29, A15, XBOOLE_0:def 4;
then y2 in (P2 ^b) /\ Q2 by A20, XBOOLE_0:def 4;
hence contradiction by A9, XBOOLE_0:def 7; :: thesis: verum

end;

P2 /\ C misses Q2 by A8, XBOOLE_1:17, XBOOLE_1:63;
then P2 /\ C misses Q2 /\ C by XBOOLE_1:17, XBOOLE_1:63;
then (P2 /\ C) ^b meets Q2 /\ C by A2, A15, A30, A22, FIN_TOPO:def 18;
then P2 ^b meets Q2 /\ C by A28, FIN_TOPO:19, XBOOLE_1:63;
hence contradiction by A9, XBOOLE_1:17, XBOOLE_1:63; :: thesis: verum