:: deftheorem defines TrivAsymOrthoRelStr OPOSET_1:def 2 :
TrivAsymOrthoRelStr = OrthoRelStr(# {0},({} ({0},{0})),op1 #);