- X = (-) X by Th25;
hence (-) X is Subset of (TOP-REAL n) ; :: thesis: verum