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

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