set A = the non empty set ;
set a = the BinOp of the non empty set ;
set Z = the Element of the non empty set ;
set r = the Function of [: the non empty set , the carrier of FS:], the non empty set ;
take
RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #)
; not RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #) is empty
thus
not the carrier of RightModStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the non empty set , the carrier of FS:], the non empty set #) is empty
; STRUCT_0:def 1 verum