:: deftheorem Def1 defines TrivOrthoRelStr OPOSET_1:def 1 :
TrivOrthoRelStr = OrthoRelStr(# {0},(id {0}),op1 #);