set b = inf (dom f);

hereby :: thesis: ( ( for a being Ordinal holds not a in dom f ) implies ex b₁ being Ordinal st b₁ = 0 )

given a being Ordinal such that a in dom f ; :: thesis: ex b being set st f is b -based
take b = inf (dom f); :: thesis: f is b -based
thus f is b -based by Th12; :: thesis: verum

end;

assume for a being Ordinal holds not a in dom f ; :: thesis: ex b₁ being Ordinal st b₁ = 0
take 0 ; :: thesis: 0 = 0
thus 0 = 0 ; :: thesis: verum