set X = the non empty set ;
set R = the Relation of the non empty set ;
set C = the UnOp of the non empty set ;
take OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) ; :: thesis: ( not OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is empty & OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is strict )
thus ( not OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is empty & OrthoRelStr(# the non empty set , the Relation of the non empty set , the UnOp of the non empty set #) is strict ) ; :: thesis: verum