let GX be TopStruct ; :: thesis: for A, B being Subset of GX st A is_a_component_of B holds
A c= B
let A, B be Subset of GX; :: thesis: ( A is_a_component_of B implies A c= B )
assume A is_a_component_of B ; :: thesis: A c= B
then A1: ex B1 being Subset of (GX | B) st
( B1 = A & B1 is a_component ) by CONNSP_1:def 6;
the carrier of (GX | B) = B by PRE_TOPC:8;
hence A c= B by A1; :: thesis: verum