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