set l = least-positive (rng v);
least-positive (rng v) in rng v by A1, Lm5;
then {(least-positive (rng v))} c= rng v by ZFMISC_1:31;
then not v " {(least-positive (rng v))} is empty by RELAT_1:139;
then the Element of v " {(least-positive (rng v))} in v " {(least-positive (rng v))} ;
hence the Element of v " {(least-positive (rng v))} is Element of K ; :: thesis: verum