defpred S₁[ set ] means $1 is Function of VAR ,D;
consider X being set such that
A1: for a being set holds
( a in X iff ( a in bool [:VAR ,D:] & S₁[a] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for a being set holds
( a in X iff a is Function of VAR ,D )
let a be set ; :: thesis: ( a in X iff a is Function of VAR ,D )
thus ( a in X implies a is Function of VAR ,D ) by A1; :: thesis: ( a is Function of VAR ,D implies a in X )
assume a is Function of VAR ,D ; :: thesis: a in X
then reconsider f = a as Function of VAR ,D ;
f in bool [:VAR ,D:] ;
hence a in X by A1; :: thesis: verum