defpred S1[ 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 & S1[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 & S1[x,y,z] ) )

assume ( x in bool X & y in bool X ) ; :: thesis: ex z being set st
( z in bool X & S1[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 & S1[x,y,x \+\ y] )
thus ( x \+\ y in bool X & S1[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
S1[x,y,f . (x,y)] from 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