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 ;
( 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 )
;
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
;
( x \+\ y in bool X & S1[x,y,x \+\ y] )
thus
(
x \+\ y in bool X &
S1[
x,
y,
x \+\ y] )
;
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 BINOP_1:sch 9(A1);
reconsider f = f as BinOp of (bool X) ;
take
f
; 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
hence
for c, d being Subset of X holds f . (c,d) = c \+\ d
; verum