let GX be TopSpace; :: thesis: for A1, A2, B being Subset of GX st A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 holds

A1 misses A2

let A1, A2, B be Subset of GX; :: thesis: ( A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 implies A1 misses A2 )

assume A1 is_a_component_of B ; :: thesis: ( not A2 is_a_component_of B or A1 = A2 or A1 misses A2 )

then A1: ex B1 being Subset of (GX | B) st

( B1 = A1 & B1 is a_component ) by CONNSP_1:def 6;

assume A2 is_a_component_of B ; :: thesis: ( A1 = A2 or A1 misses A2 )

then ex B2 being Subset of (GX | B) st

( B2 = A2 & B2 is a_component ) by CONNSP_1:def 6;

hence ( A1 = A2 or A1 misses A2 ) by A1, CONNSP_1:35; :: thesis: verum

A1 misses A2

let A1, A2, B be Subset of GX; :: thesis: ( A1 is_a_component_of B & A2 is_a_component_of B & not A1 = A2 implies A1 misses A2 )

assume A1 is_a_component_of B ; :: thesis: ( not A2 is_a_component_of B or A1 = A2 or A1 misses A2 )

then A1: ex B1 being Subset of (GX | B) st

( B1 = A1 & B1 is a_component ) by CONNSP_1:def 6;

assume A2 is_a_component_of B ; :: thesis: ( A1 = A2 or A1 misses A2 )

then ex B2 being Subset of (GX | B) st

( B2 = A2 & B2 is a_component ) by CONNSP_1:def 6;

hence ( A1 = A2 or A1 misses A2 ) by A1, CONNSP_1:35; :: thesis: verum