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 & A1 is connected & A2 is connected ) and
A2: ( A0 meets A1 & A1 meets A2 ) ; :: thesis: (A0 \/ A1) \/ A2 is connected
A3: ( A0 /\ A1 <> {} & A1 /\ A2 <> {} ) by A2, XBOOLE_0:def 7;
A4: A0 \/ A1 is connected by A1, A2, CONNSP_1:2, CONNSP_1:18;
(A0 \/ A1) /\ A2 = (A0 /\ A2) \/ (A1 /\ A2) by XBOOLE_1:23;
then (A0 \/ A1) /\ A2 <> {} by A3;
then A0 \/ A1 meets A2 by XBOOLE_0:def 7;
hence (A0 \/ A1) \/ A2 is connected by A1, A4, CONNSP_1:2, CONNSP_1:18; :: thesis: verum