set b = sup (dom f);
hereby :: thesis: ( ( for a being Ordinal holds not a in dom f ) implies ex b1 being Ordinal st b1 = 0 )
given a being Ordinal such that a in dom f ; :: thesis: ex b being set st f is b -limited
take b = sup (dom f); :: thesis: f is b -limited
thus f is b -limited ; :: thesis: verum
end;
assume for a being Ordinal holds not a in dom f ; :: thesis: ex b1 being Ordinal st b1 = 0
take 0 ; :: thesis: 0 = 0
thus 0 = 0 ; :: thesis: verum