consider A being non empty set , m being BinOp of A;
take MidStr(# A,m #) ; :: thesis: not MidStr(# A,m #) is empty
thus not the carrier of MidStr(# A,m #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum