let T be non empty TopSpace; :: thesis: for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds
x is_a_convergence_point_of G,T
let F, G, x be set ; :: thesis: ( F c= G & x is_a_convergence_point_of F,T implies x is_a_convergence_point_of G,T )
assume that
A1: F c= G and
A2: for A being Subset of T st A is open & x in A holds
A in F ; :: according to WAYBEL_7:def 5 :: thesis: x is_a_convergence_point_of G,T
let A be Subset of T; :: according to WAYBEL_7:def 5 :: thesis: ( not A is open or not x in A or A in G )
assume ( A is open & x in A ) ; :: thesis: A in G
then A in F by A2;
hence A in G by A1; :: thesis: verum