let M be Cardinal; :: thesis: M +` 0 = M
A1: [:{} ,{1}:] = {} by ZFMISC_1:113;
thus M +` 0 = card H₃(M, {} ) by Lm1
.= card M by A1, Th13
.= M by CARD_1:def 5 ; :: thesis: verum