let S, T be TopStruct ; :: thesis: for F being Subset-Family of S
for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
let F be Subset-Family of S; :: thesis: for G being Subset-Family of T st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed holds
G is closed
let G be Subset-Family of T; :: thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & F = G & F is closed implies G is closed )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: ( F = G & F is closed ) ; :: thesis: G is closed
let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in G or P is closed )
assume A3: P in G ; :: thesis: P is closed
reconsider R = P as Subset of S by A1;
R is closed by A2, A3;
then ([#] S) \ R is open ;
hence ([#] T) \ P in the topology of T by A1; :: according to PRE_TOPC:def 2,PRE_TOPC:def 3 :: thesis: verum