let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A c= B holds

A ^0 c= B ^0

let A, B be Subset of T; :: thesis: ( A c= B implies A ^0 c= B ^0 )

assume A1: A c= B ; :: thesis: A ^0 c= B ^0

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^0 or x in B ^0 )

assume A2: x in A ^0 ; :: thesis: x in B ^0

then reconsider x9 = x as Point of T ;

x9 is_a_condensation_point_of A by A2, Def10;

then x9 is_a_condensation_point_of B by A1, Th48;

hence x in B ^0 by Def10; :: thesis: verum

A ^0 c= B ^0

let A, B be Subset of T; :: thesis: ( A c= B implies A ^0 c= B ^0 )

assume A1: A c= B ; :: thesis: A ^0 c= B ^0

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^0 or x in B ^0 )

assume A2: x in A ^0 ; :: thesis: x in B ^0

then reconsider x9 = x as Point of T ;

x9 is_a_condensation_point_of A by A2, Def10;

then x9 is_a_condensation_point_of B by A1, Th48;

hence x in B ^0 by Def10; :: thesis: verum