consider A being non empty set , C, o being Relation of [:A,A:];
take ParOrtStr(# A,C,o #) ; :: thesis: not ParOrtStr(# A,C,o #) is empty
thus not the carrier of ParOrtStr(# A,C,o #) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum