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 consider B1 being Subset of (GX | B) such that
A1: B1 = A1 and
A2: B1 is_a_component_of GX | B 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_of GX | B ) by CONNSP_1:def 6;
hence ( A1 = A2 or A1 misses A2 ) by A1, A2, CONNSP_1:37; :: thesis: verum