defpred S₁[ set ] means ex x being bound_QC-variable st
( x = $1 & x in still_not-bound_in p & x = (@ Sub) . x );
consider X being set such that
A1: for b being set holds
( b in X iff ( b in bound_QC-variables & S₁[b] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for b being set holds
( b in X iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) )
thus for b being set holds
( b in X iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) by A1; :: thesis: verum