let X be non empty anti-discrete TopSpace; :: thesis: for A being Subset of X holds
( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) )
let A be Subset of X; :: thesis: ( ( A <> {} implies A is dense ) & ( A <> the carrier of X implies A is boundary ) )
thus ( A <> {} implies A is dense ) :: thesis: ( A <> the carrier of X implies A is boundary )
proof
assume A <> {} ; :: thesis: A is dense
then Cl A = the carrier of X by Th9;
hence A is dense by TOPS_3:def 2; :: thesis: verum
end;
thus ( A <> the carrier of X implies A is boundary ) :: thesis: verum
proof
assume A <> the carrier of X ; :: thesis: A is boundary
then Int A = {} by Th10;
hence A is boundary by TOPS_1:48; :: thesis: verum
end;