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 that
A3: A is open and
A4: x in A ; :: thesis: A in G
A in F by A2, A3, A4;
hence A in G by A1; :: thesis: verum