let T be TopSpace; :: thesis: for X being Subset of
for Y being Subset of 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 ; :: thesis: for Y being Subset of 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 ; :: 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 A1: 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 A2: 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 Def5;
hence Y is connected by A1, Th47; :: according to CONNSP_1:def 5 :: thesis: for B being Subset of st B is connected & Y c= B holds
Y = B
let B be Subset of ; :: thesis: ( B is connected & Y c= B implies Y = B )
assume that
A3: B is connected and
A4: Y c= B ; :: thesis: Y = B
reconsider C = B as Subset of ;
C is connected by A3, Th47;
hence Y = B by A1, A2, A4, Def5; :: thesis: verum

end;

assume A5: 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 Def5;
hence X is connected by A1, Th47; :: according to CONNSP_1:def 5 :: thesis: for B being Subset of st B is connected & X c= B holds
X = B
let B be Subset of ; :: thesis: ( B is connected & X c= B implies X = B )
assume that
A6: B is connected and
A7: X c= B ; :: thesis: X = B
reconsider C = B as Subset of ;
C is connected by A6, Th47;
hence X = B by A1, A5, A7, Def5; :: thesis: verum