:: deftheorem defines TrivLattRelStr ROBBINS3:def 4 :
TrivLattRelStr = LattRelStr(# {0},op2,op2,(id {0}) #);