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 consider B1 being Subset of (GX | B) such that
A1: B1 = A and
B1 is_a_component_of GX | B by CONNSP_1:def 6;
the carrier of (GX | B) = B by PRE_TOPC:29;
hence A c= B by A1; :: thesis: verum