consider X being set such that
A1: for a being object holds
( a in X iff ( a in Aux L & S1[a] ) ) from XBOOLE_0:sch 1();
 take X ; :: thesis: for a being set holds
( a in X iff a is auxiliary approximating Relation of L )
for a being set st a is auxiliary approximating Relation of L holds
a in X
proof
let a be set ; :: thesis: ( a is auxiliary approximating Relation of L implies a in X )
assume A2: a is auxiliary approximating Relation of L ; :: thesis: a in X
then a in Aux L by Def8;
hence a in X by A1, A2; :: thesis: verum
end;
hence for a being set holds
( a in X iff a is auxiliary approximating Relation of L ) by A1; :: thesis: verum