a in On W by ORDINAL1:def 9;
then a in dom L by Def2;
then A4: L . a in rng L by FUNCT_1:def 3;
thus L . a is non empty Element of W by A4, RELAT_1:def 9; :: thesis: verum