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 open holds
G is open
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 open holds
G is open
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 open implies G is open )
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 and
A3: F is open ; :: thesis: G is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in G or P is open )
assume A4: P in G ; :: thesis: P is open
reconsider R = P as Subset of S by A1;
R is open by A2, A3, A4, TOPS_2:def 1;
hence P in the topology of T by A1, PRE_TOPC:def 5; :: according to PRE_TOPC:def 5 :: thesis: verum