let GX be non empty TopSpace; :: thesis: for A0, A1, A2, A3 being Subset of GX st A0 is connected & A1 is connected & A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 & A2 meets A3 holds
((A0 \/ A1) \/ A2) \/ A3 is connected
let A0, A1, A2, A3 be Subset of GX; :: thesis: ( A0 is connected & A1 is connected & A2 is connected & A3 is connected & A0 meets A1 & A1 meets A2 & A2 meets A3 implies ((A0 \/ A1) \/ A2) \/ A3 is connected )
assume that
A1: ( A0 is connected & A1 is connected & A2 is connected & A3 is connected ) and
A2: ( A0 meets A1 & A1 meets A2 & A2 meets A3 ) ; :: thesis: ((A0 \/ A1) \/ A2) \/ A3 is connected
A3: ( A0 /\ A1 <> {} & A1 /\ A2 <> {} & A2 /\ A3 <> {} ) by A2, XBOOLE_0:def 7;
A4: (A0 \/ A1) \/ A2 is connected by A1, A2, Th7;
((A0 \/ A1) \/ A2) /\ A3 = ((A0 \/ A1) /\ A3) \/ (A2 /\ A3) by XBOOLE_1:23;
then ((A0 \/ A1) \/ A2) /\ A3 <> {} by A3;
then (A0 \/ A1) \/ A2 meets A3 by XBOOLE_0:def 7;
hence ((A0 \/ A1) \/ A2) \/ A3 is connected by A1, A4, CONNSP_1:2, CONNSP_1:18; :: thesis: verum