let M1, M2 be set ; :: thesis: ( card M1 = 0 & card M2 = 0 implies M1 = M2 )
assume ( card M1 = {} & card M2 = {} ) ; :: thesis: M1 = M2
then ( M1 = {} & M2 = {} ) ;
hence M1 = M2 ; :: thesis: verum