:: deftheorem defines TrivComplLat ROBBINS1:def 1 :
TrivComplLat = ComplLLattStr(# {0},op2,op1 #);