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 and
A2: A1 is connected and
A3: A2 is connected and
A4: A3 is connected and
A5: A0 meets A1 and
A6: A1 meets A2 and
A7: A2 meets A3 ; :: thesis: ((A0 \/ A1) \/ A2) \/ A3 is connected
A8: A2 /\ A3 <> {} by A7;
A9: (A0 \/ A1) \/ A2 is connected by A1, A2, A3, A5, A6, Th4;
((A0 \/ A1) \/ A2) /\ A3 = ((A0 \/ A1) /\ A3) \/ (A2 /\ A3) by XBOOLE_1:23;
then (A0 \/ A1) \/ A2 meets A3 by A8;
hence ((A0 \/ A1) \/ A2) \/ A3 is connected by A4, A9, CONNSP_1:1, CONNSP_1:17; :: thesis: verum