:: deftheorem defines TrivOrtLat ROBBINS1:def 2 :
TrivOrtLat = OrthoLattStr(# {0},op2,op2,op1 #);