let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds

A \/ B c= Component_of A

let A, B be Subset of GX; :: thesis: ( A is connected & A \/ B is connected & A <> {} implies A \/ B c= Component_of A )

assume that

A1: A is connected and

A2: A \/ B is connected and

A3: A <> {} ; :: thesis: A \/ B c= Component_of A

Component_of (A \/ B) = Component_of A by A1, A2, A3, Th12, XBOOLE_1:7;

hence A \/ B c= Component_of A by A2, Th1; :: thesis: verum

A \/ B c= Component_of A

let A, B be Subset of GX; :: thesis: ( A is connected & A \/ B is connected & A <> {} implies A \/ B c= Component_of A )

assume that

A1: A is connected and

A2: A \/ B is connected and

A3: A <> {} ; :: thesis: A \/ B c= Component_of A

Component_of (A \/ B) = Component_of A by A1, A2, A3, Th12, XBOOLE_1:7;

hence A \/ B c= Component_of A by A2, Th1; :: thesis: verum