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