let X be set ; :: thesis: ( X is empty implies X is 0 -element )
assume X is empty ; :: thesis: X is 0 -element
then card X = {} ;
hence X is 0 -element by Def13; :: thesis: verum