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 object such that
A2: x1 in the carrier of X and
A3: W1 = Class (E,x1) by EQREL_1:def 3;
consider y1 being object such that
A4: y1 in the carrier of X and
A5: W2 = Class (E,y1) by EQREL_1:def 3;
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 3;
take C ; :: thesis: S₁[W1,W2,C]

now :: thesis: for x, y being Element of X st W1 = Class (E,x) & W2 = Class (E,y) holds
C = Class (E,(x \ y))

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:23;
then A8: [y1,y] in E by EQREL_1:18;
x in Class (E,x1) by A3, A6, EQREL_1:23;
then [x1,x] in E by EQREL_1:18;
then [(x1 \ y1),(x \ y)] in E by A8, Def9;
then x \ y in Class (E,(x1 \ y1)) by EQREL_1:18;
hence C = Class (E,(x \ y)) by EQREL_1:23; :: 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