defpred S₁[ set , set , set ] means ex a, b being Subset of X st
( $1 = a & $2 = b & $3 = a \+\ b );
A1: for x, y being set st x in bool X & y in bool X holds
ex z being set st
( z in bool X & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in bool X & y in bool X implies ex z being set st
( z in bool X & S₁[x,y,z] ) )
assume ( x in bool X & y in bool X ) ; :: thesis: ex z being set st
( z in bool X & S₁[x,y,z] )
then reconsider x = x, y = y as Subset of X ;
set z = x \+\ y;
take x \+\ y ; :: thesis: ( x \+\ y in bool X & S₁[x,y,x \+\ y] )
thus ( x \+\ y in bool X & S₁[x,y,x \+\ y] ) ; :: thesis: verum

end;

consider f being Function of [:(bool X),(bool X):],(bool X) such that
A2: for x, y being set st x in bool X & y in bool X holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 9(A1);
reconsider f = f as BinOp of (bool X) ;
take f ; :: thesis: for c, d being Subset of X holds f . (c,d) = c \+\ d
for c, d being Subset of X holds f . (c,d) = c \+\ d

proof

let c, d be Subset of X; :: thesis: f . (c,d) = c \+\ d
ex a, b being Subset of X st
( c = a & d = b & f . (c,d) = a \+\ b ) by A2;
hence f . (c,d) = c \+\ d ; :: thesis: verum

end;

hence for c, d being Subset of X holds f . (c,d) = c \+\ d ; :: thesis: verum