let M1, M2 be set ; :: thesis: ( card M1 = 0 & card M2 = 0 implies M1 = M2 )
assume that
A1: card M1 = 0 and
A2: card M2 = 0 ; :: thesis: M1 = M2
M1 = {} by A1;
hence M1 = M2 by A2; :: thesis: verum