let M1, M2 be cardinal number ; ( ex B being Basis of x st M1 = card B & ( for B being Basis of x holds M1 c= card B ) & ex B being Basis of x st M2 = card B & ( for B being Basis of x holds M2 c= card B ) implies M1 = M2 )
assume that
A5:
ex B being Basis of x st M1 = card B
and
A6:
for B being Basis of x holds M1 c= card B
and
A7:
ex B being Basis of x st M2 = card B
and
A8:
for B being Basis of x holds M2 c= card B
; M1 = M2
thus
( M1 c= M2 & M2 c= M1 )
by A5, A6, A7, A8; XBOOLE_0:def 10 verum