take [#] GX ; :: thesis: ( not [#] GX is boundary & not [#] GX is empty )
thus ( not [#] GX is boundary & not [#] GX is empty ) ; :: thesis: verum