defpred S₁[ set ] means $1 is Division of A;
consider R being set such that
A1: for x1 being set holds
( x1 in R iff ( x1 in bool [:NAT,REAL:] & S₁[x1] ) ) from XFAMILY:sch 1();
take R ; :: thesis: for x1 being set holds
( x1 in R iff x1 is Division of A )
let x1 be set ; :: thesis: ( x1 in R iff x1 is Division of A )
thus ( x1 in R implies x1 is Division of A ) by A1; :: thesis: ( x1 is Division of A implies x1 in R )
assume x1 is Division of A ; :: thesis: x1 in R
then reconsider p = x1 as Division of A ;
p c= [:NAT,REAL:] ;
hence x1 in R by A1; :: thesis: verum