let A be Subset of GX; :: thesis: ( A is empty implies A is boundary )
assume A is empty ; :: thesis: A is boundary
hence Cl (A `) = [#] GX by Th2; :: according to TOPS_1:def 3,TOPS_1:def 4 :: thesis: verum