let FT be non empty RelStr ; 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; ( 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
; A is connected
let P2, Q2 be Subset of FT; FIN_TOPO:def 16 ( 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
; not P2 ^b misses Q2
assume A9:
P2 ^b misses Q2
; 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;
A28:
P2 /\ C c= P2
by XBOOLE_1:17;
A29:
y2 in C
by A19, XBOOLE_0:def 4;
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; verum