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 16 :: 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
set x2 = the Element of Q2;
A10: the Element of Q2 in Q2 by A7;
Q2 c= Q2 \/ P2 by XBOOLE_1:7;
then Q2 c= C ^b by A4, A5;
then the Element of Q2 in C ^b by A10;
then consider z2 being Element of FT such that
A11: z2 = the Element of Q2 and
A12: U_FT z2 meets C ;
set y3 = the Element of (U_FT z2) /\ C;
A13: (U_FT z2) /\ C <> {} by A12;
then the Element of (U_FT z2) /\ C in (U_FT z2) /\ C ;
then reconsider y4 = the Element of (U_FT z2) /\ C as Element of FT ;
the Element of (U_FT z2) /\ C in U_FT z2 by A13, XBOOLE_0:def 4;
then z2 in U_FT y4 by A1;
then z2 in (U_FT y4) /\ Q2 by A7, A11, XBOOLE_0:def 4;
then A14: U_FT y4 meets Q2 ;
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 ;
set x = the Element of P2;
A16: the Element of P2 in P2 by A6;
P2 c= P2 \/ Q2 by XBOOLE_1:7;
then P2 c= C ^b by A4, A5;
then the Element of P2 in C ^b by A16;
then consider z being Element of FT such that
A17: z = the Element of P2 and
A18: U_FT z meets C ;
set y = the Element of (U_FT z) /\ C;
A19: (U_FT z) /\ C <> {} by A18;
then the Element of (U_FT z) /\ C in (U_FT z) /\ C ;
then reconsider y2 = the Element of (U_FT z) /\ C as Element of FT ;
the Element of (U_FT z) /\ C in U_FT z by A19, XBOOLE_0:def 4;
then z in U_FT y2 by A1;
then z in (U_FT y2) /\ P2 by A6, A17, XBOOLE_0:def 4;
then U_FT y2 meets P2 ;
then A20: y2 in P2 ^b ;
A21: y4 in C by A13, XBOOLE_0:def 4;

A22: now :: thesis: not Q2 /\ C = {}

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 object 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;
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 :: thesis: not P2 /\ C = {}

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; :: 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;
then P2 ^b meets Q2 /\ C by A28, FIN_TOPO:14, XBOOLE_1:63;
hence contradiction by A9, XBOOLE_1:17, XBOOLE_1:63; :: thesis: verum