consider A being non empty set , m being BinOp of A, h being Action of O,A;
take HGrWOpStr(# A,m,h #) ; :: thesis: not HGrWOpStr(# A,m,h #) is empty
thus not HGrWOpStr(# A,m,h #) is empty ; :: thesis: verum