set a = the auxiliary approximating Relation of L;
the auxiliary approximating Relation of L in App L by Def19;
hence not App L is empty ; :: thesis: verum