defpred S₁[ set ] means $1 is auxiliary Relation of L;
consider X being set such that
A1: for a being set holds
( a in X iff ( a in bool [: the carrier of L, the carrier of L:] & S₁[a] ) ) from XFAMILY:sch 1();
take X ; :: thesis: for a being set holds
( a in X iff a is auxiliary Relation of L )
thus for a being set holds
( a in X iff a is auxiliary Relation of L ) by A1; :: thesis: verum