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