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