let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for x being set st A c= B & x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
let A, B be Subset of T; :: thesis: for x being set st A c= B & x is_an_accumulation_point_of A holds
x is_an_accumulation_point_of B
let x be set ; :: thesis: ( A c= B & x is_an_accumulation_point_of A implies x is_an_accumulation_point_of B )
assume A c= B ; :: thesis: ( not x is_an_accumulation_point_of A or x is_an_accumulation_point_of B )
then A1: Der A c= Der B by Th30;
assume x is_an_accumulation_point_of A ; :: thesis: x is_an_accumulation_point_of B
then x in Der A by Th16;
hence x is_an_accumulation_point_of B by A1, Th16; :: thesis: verum