per cases ( not D is empty or D is empty ) ;
suppose not D is empty ; :: thesis: [:D,D:] --> the Element of D is BinOp of D
then reconsider D = D as non empty set ;
[:D,D:] --> the Element of D is BinOp of D ;
hence [:D,D:] --> the Element of D is BinOp of D ; :: thesis: verum
end;
suppose D is empty ; :: thesis: [:D,D:] --> the Element of D is BinOp of D
hence [:D,D:] --> the Element of D is BinOp of D ; :: thesis: verum
end;
end;