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