defpred S_{1}[ 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_{1}[x,y,z] )

A2: for x, y being set st x in bool X & y in bool X holds

S_{1}[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

( $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

proof

consider f being Function of [:(bool X),(bool X):],(bool X) such that
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_{1}[x,y,z] ) )

assume ( x in bool X & y in bool X ) ; :: thesis: ex z being set st

( z in bool X & S_{1}[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_{1}[x,y,x \+\ y] )

thus ( x \+\ y in bool X & S_{1}[x,y,x \+\ y] )
; :: thesis: verum

end;( z in bool X & S

assume ( x in bool X & y in bool X ) ; :: thesis: ex z being set st

( z in bool X & S

then reconsider x = x, y = y as Subset of X ;

set z = x \+\ y;

take x \+\ y ; :: thesis: ( x \+\ y in bool X & S

thus ( x \+\ y in bool X & S

A2: for x, y being set st x in bool X & y in bool X holds

S

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

hence
for c, d being Subset of X holds f . (c,d) = c \+\ d
; :: thesis: verum
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;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