let T be TopSpace; :: thesis: for X being Subset of T
for Y being Subset of TopStruct(# the carrier of T,the topology of T #) st X = Y holds
( X is_a_component_of T iff Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) )
let X be Subset of T; :: thesis: for Y being Subset of TopStruct(# the carrier of T,the topology of T #) st X = Y holds
( X is_a_component_of T iff Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) )
let Y be Subset of TopStruct(# the carrier of T,the topology of T #); :: thesis: ( X = Y implies ( X is_a_component_of T iff Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) ) )
assume Z0: X = Y ; :: thesis: ( X is_a_component_of T iff Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) )
thus ( X is_a_component_of T implies Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) ) :: thesis: ( Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) implies X is_a_component_of T )

proof

assume Z: X is_a_component_of T ; :: thesis: Y is_a_component_of TopStruct(# the carrier of T,the topology of T #)
then X is connected by Z0, Def5;
hence Y is connected by Z0, Th47; :: according to CONNSP_1:def 5 :: thesis: for B being Subset of TopStruct(# the carrier of T,the topology of T #) st B is connected & Y c= B holds
Y = B
let B be Subset of TopStruct(# the carrier of T,the topology of T #); :: thesis: ( B is connected & Y c= B implies Y = B )
assume that
Z1: B is connected and
Z2: Y c= B ; :: thesis: Y = B
reconsider C = B as Subset of T ;
C is connected by Z1, Th47;
then C = X by Z2, Z0, Def5, Z;
hence Y = B by Z0; :: thesis: verum

end;

assume Z: Y is_a_component_of TopStruct(# the carrier of T,the topology of T #) ; :: thesis: X is_a_component_of T
then Y is connected by Z0, Def5;
hence X is connected by Z0, Th47; :: according to CONNSP_1:def 5 :: thesis: for B being Subset of T st B is connected & X c= B holds
X = B
let B be Subset of T; :: thesis: ( B is connected & X c= B implies X = B )
assume that
Z1: B is connected and
Z2: X c= B ; :: thesis: X = B
reconsider C = B as Subset of TopStruct(# the carrier of T,the topology of T #) ;
C is connected by Z1, Th47;
then C = X by Z2, Z0, Def5, Z;
hence X = B by Z0; :: thesis: verum