let T be TopSpace; :: thesis: for X being set holds
( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )
let X be set ; :: thesis: ( X is connected Subset of T iff X is connected Subset of TopStruct(# the carrier of T, the topology of T #) )
thus ( X is connected Subset of T implies X is connected Subset of TopStruct(# the carrier of T, the topology of T #) ) :: thesis: ( X is connected Subset of TopStruct(# the carrier of T, the topology of T #) implies X is connected Subset of T )
proof
assume A1: X is connected Subset of T ; :: thesis: X is connected Subset of TopStruct(# the carrier of T, the topology of T #)
then reconsider X = X as Subset of T ;
reconsider Y = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
TopStruct(# the carrier of (T | X), the topology of (T | X) #) = TopStruct(# the carrier of T, the topology of T #) | Y by PRE_TOPC:36;
then TopStruct(# the carrier of T, the topology of T #) | Y is connected by A1, Def3;
hence X is connected Subset of TopStruct(# the carrier of T, the topology of T #) by Def3; :: thesis: verum
end;
assume A2: X is connected Subset of TopStruct(# the carrier of T, the topology of T #) ; :: thesis: X is connected Subset of T
then reconsider X = X as Subset of TopStruct(# the carrier of T, the topology of T #) ;
reconsider Y = X as Subset of T ;
TopStruct(# the carrier of (T | Y), the topology of (T | Y) #) = TopStruct(# the carrier of T, the topology of T #) | X by PRE_TOPC:36;
then T | Y is connected by A2, Def3;
hence X is connected Subset of T by Def3; :: thesis: verum