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 iff Y is a_component )
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 iff Y is a_component )
let Y be Subset of TopStruct(# the carrier of T, the topology of T #); :: thesis: ( X = Y implies ( X is a_component iff Y is a_component ) )
assume A1: X = Y ; :: thesis: ( X is a_component iff Y is a_component )
thus ( X is a_component implies Y is a_component ) :: thesis: ( Y is a_component implies X is a_component )

proof

assume A2: X is a_component ; :: thesis: Y is a_component
hence Y is connected by A1, 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
A3: B is connected and
A4: Y c= B ; :: thesis: Y = B
reconsider C = B as Subset of T ;
C is connected by A3, Th47;
hence Y = B by A1, A2, A4, Def5; :: thesis: verum

end;

assume A5: Y is a_component ; :: thesis: X is a_component
hence X is connected by A1, 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
A6: B is connected and
A7: 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 A6, Th47;
hence X = B by A1, A5, A7, Def5; :: thesis: verum