let M1, M2 be cardinal number ; ( ( for x being Point of T holds Chi (x,T) c= M1 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M1 c= M ) & ( for x being Point of T holds Chi (x,T) c= M2 ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M2 c= M ) implies M1 = M2 )
assume that
A1:
for x being Point of T holds Chi (x,T) c= M1
and
A2:
for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M1 c= M
and
A3:
for x being Point of T holds Chi (x,T) c= M2
and
A4:
for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
M2 c= M
; M1 = M2
thus
( M1 c= M2 & M2 c= M1 )
by A1, A2, A3, A4; XBOOLE_0:def 10 verum