consider B being Ordinal such that
A1: rng L c= B by Def4;
L | A is Ordinal-yielding

proof

take B ; :: according to ORDINAL2:def 4 :: thesis: rng (L | A) c= B
rng (L | A) c= rng L by RELAT_1:70;
hence rng (L | A) c= B by A1; :: thesis: verum

end;

hence L | A is Ordinal-yielding ; :: thesis: verum