defpred S₁[ Element of Class E, Element of Class E, set ] means for x, y being Element of X st $1 = Class E,x & $2 = Class E,y holds
$3 = Class E,(x \ y);
A1: for W1, W2 being Element of Class E ex V being Element of Class E st S₁[W1,W2,V]

proof

let W1, W2 be Element of Class E; :: thesis: ex V being Element of Class E st S₁[W1,W2,V]
consider x1 being set such that
A2: x1 in the carrier of X and
A3: W1 = Class E,x1 by EQREL_1:def 5;
consider y1 being set such that
A4: y1 in the carrier of X and
A5: W2 = Class E,y1 by EQREL_1:def 5;
reconsider x1 = x1, y1 = y1 as Element of X by A2, A4;
reconsider C = Class E,(x1 \ y1) as Element of Class E by EQREL_1:def 5;
take C ; :: thesis: S₁[W1,W2,C]

now

let x, y be Element of X; :: thesis: ( W1 = Class E,x & W2 = Class E,y implies C = Class E,(x \ y) )
assume that
A6: W1 = Class E,x and
A7: W2 = Class E,y ; :: thesis: C = Class E,(x \ y)
y in Class E,y1 by A5, A7, EQREL_1:31;
then A8: [y1,y] in E by EQREL_1:26;
x in Class E,x1 by A3, A6, EQREL_1:31;
then [x1,x] in E by EQREL_1:26;
then [(x1 \ y1),(x \ y)] in E by A8, Def9;
then x \ y in Class E,(x1 \ y1) by EQREL_1:26;
hence C = Class E,(x \ y) by EQREL_1:31; :: thesis: verum

end;

hence S₁[W1,W2,C] ; :: thesis: verum

end;

thus ex B being BinOp of (Class E) st
for W1, W2 being Element of Class E holds S₁[W1,W2,B . W1,W2] from BINOP_1:sch 3(A1); :: thesis: verum