consider a being auxiliary approximating Relation of L;
a in App L by Def20;
hence not App L is empty ; :: thesis: verum