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;

A29: y2 in C by A19, XBOOLE_0:def 4;

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

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 = {}

A28:
P2 /\ C c= P2
by XBOOLE_1:17;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;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

A29: y2 in C by A19, XBOOLE_0:def 4;

A30: now :: thesis: not P2 /\ C = {}

P2 /\ C misses Q2
by A8, XBOOLE_1:17, XBOOLE_1:63;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;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

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