let M1, M2 be cardinal number ; :: thesis: ( ( 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 ; :: thesis: M1 = M2
thus ( M1 c= M2 & M2 c= M1 ) by A1, A2, A3, A4; :: according to XBOOLE_0:def 10 :: thesis: verum