let T be TopSpace; :: thesis: for X being set holds
( X is connected Subset of iff X is connected Subset of )
let X be set ; :: thesis: ( X is connected Subset of iff X is connected Subset of )
thus ( X is connected Subset of implies X is connected Subset of ) :: thesis: ( X is connected Subset of implies X is connected Subset of )

proof

assume A1: X is connected Subset of ; :: thesis: X is connected Subset of
then reconsider X = X as Subset of ;
reconsider Y = X as Subset of ;
TopStruct(# the carrier of (T | X),the topology of (T | X) #) = TopStruct(# the carrier of T,the topology of T #) | Y by PRE_TOPC:66;
then TopStruct(# the carrier of T,the topology of T #) | Y is connected by A1, Def3;
hence X is connected Subset of by Def3; :: thesis: verum

end;

assume A2: X is connected Subset of ; :: thesis: X is connected Subset of
then reconsider X = X as Subset of ;
reconsider Y = X as Subset of ;
TopStruct(# the carrier of (T | Y),the topology of (T | Y) #) = TopStruct(# the carrier of T,the topology of T #) | X by PRE_TOPC:66;
then T | Y is connected by A2, Def3;
hence X is connected Subset of by Def3; :: thesis: verum