let B be Subset of (TOP-REAL 2); :: thesis: ( B = {(0. (TOP-REAL 2))} implies ( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} ) )
assume A1: B = {(0. (TOP-REAL 2))} ; :: thesis: ( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} )

now :: thesis: not |[0,1]| in B

assume |[0,1]| in B ; :: thesis: contradiction
then |[0,1]| `2 = 0 by A1, Th3, TARSKI:def 1;
hence contradiction by EUCLID:52; :: thesis: verum

end;

then |[0,1]| in the carrier of (TOP-REAL 2) \ B by XBOOLE_0:def 5;
hence ( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} ) by SUBSET_1:def 4; :: thesis: verum