:: deftheorem defines TrivCLRelStr ROBBINS3:def 5 :
TrivCLRelStr = OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #);