set X = { (Chi (x,T)) where x is Point of T : verum } ;
reconsider m = union { (Chi (x,T)) where x is Point of T : verum } as cardinal number by Lm1;
take m ; :: thesis: ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) )
thus ( ( for x being Point of T holds Chi (x,T) c= m ) & ( for M being cardinal number st ( for x being Point of T holds Chi (x,T) c= M ) holds
m c= M ) ) by Lm1; :: thesis: verum