:: deftheorem Def19 defines App WAYBEL_4:def 19 :
for L being complete LATTICE
for b₂ being set holds
( b₂ = App L iff for a being set holds
( a in b₂ iff a is auxiliary approximating Relation of L ) );