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 )

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

( 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 A2:
X is connected Subset of TopStruct(# the carrier of T, the topology of T #)
; :: thesis: X is connected Subset of T
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;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

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