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;