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 A5: ( A = P2 \/ Q2 & P2 <> {} & Q2 <> {} & P2 misses Q2 ) ; :: thesis: not P2 ^b misses Q2
assume A6: P2 ^b misses Q2 ; :: thesis: contradiction
P2 c= P2 \/ Q2 by XBOOLE_1:7;
then A7: P2 c= C ^b by A4, A5, XBOOLE_1:1;
consider x being Element of P2;
x in P2 by A5;
then x in C ^b by A7;
then consider z being Element of FT such that
A8: ( z = x & U_FT z meets C ) ;
A9: (U_FT z) /\ C <> {} by A8, XBOOLE_0:def 7;
consider y being Element of (U_FT z) /\ C;
A10: y in (U_FT z) /\ C by A9;
A11: ( y in U_FT z & y in C ) by A9, XBOOLE_0:def 4;
reconsider y2 = y as Element of FT by A10;
z in U_FT y2 by A1, A11, FIN_TOPO:def 15;
then z in (U_FT y2) /\ P2 by A5, A8, XBOOLE_0:def 4;
then U_FT y2 meets P2 by XBOOLE_0:def 7;
then A12: y2 in P2 ^b ;
A13: y2 in C by A9, XBOOLE_0:def 4;
Q2 c= Q2 \/ P2 by XBOOLE_1:7;
then A14: Q2 c= C ^b by A4, A5, XBOOLE_1:1;
consider x2 being Element of Q2;
x2 in Q2 by A5;
then x2 in C ^b by A14;
then consider z2 being Element of FT such that
A15: ( z2 = x2 & U_FT z2 meets C ) ;
A16: (U_FT z2) /\ C <> {} by A15, XBOOLE_0:def 7;
consider y3 being Element of (U_FT z2) /\ C;
A17: y3 in (U_FT z2) /\ C by A16;
A18: ( y3 in U_FT z2 & y3 in C ) by A16, XBOOLE_0:def 4;
reconsider y4 = y3 as Element of FT by A17;
z2 in U_FT y4 by A1, A18, FIN_TOPO:def 15;
then z2 in (U_FT y4) /\ Q2 by A5, A15, XBOOLE_0:def 4;
then A19: U_FT y4 meets Q2 by XBOOLE_0:def 7;
A20: y4 in C by A16, XBOOLE_0:def 4;
set P3 = P2 /\ C;
set Q3 = Q2 /\ C;
A21: C = A /\ C by A3, XBOOLE_1:28
.= (P2 /\ C) \/ (Q2 /\ C) by A5, XBOOLE_1:23 ;
P2 /\ C misses Q2 by A5, XBOOLE_1:17, XBOOLE_1:63;
then A22: P2 /\ C misses Q2 /\ C by XBOOLE_1:17, XBOOLE_1:63;

A23: now

assume P2 /\ C = {} ; :: thesis: contradiction
then y2 in Q2 by A13, A21, XBOOLE_0:def 4;
then y2 in (P2 ^b ) /\ Q2 by A12, XBOOLE_0:def 4;
hence contradiction by A6, XBOOLE_0:def 7; :: thesis: verum

end;

now

assume Q2 /\ C = {} ; :: thesis: contradiction
then A24: y4 in P2 by A20, A21, XBOOLE_0:def 4;
consider w being Element of FT such that
A25: ( w = y4 & U_FT w meets Q2 ) by A19;
consider s being set such that
A26: ( s in U_FT w & 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 A24, A25, XBOOLE_0:3;
then s2 in P2 ^b ;
hence contradiction by A6, A26, XBOOLE_0:3; :: thesis: verum

end;

then A27: (P2 /\ C) ^b meets Q2 /\ C by A2, A21, A22, A23, FIN_TOPO:def 18;
P2 /\ C c= P2 by XBOOLE_1:17;
then P2 ^b meets Q2 /\ C by A27, FIN_TOPO:19, XBOOLE_1:63;
hence contradiction by A6, XBOOLE_1:17, XBOOLE_1:63; :: thesis: verum