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