:: deftheorem defines Trivial-RLSStruct RLVECT_1:def 9 :
Trivial-RLSStruct = RLSStruct(# {0},op0,op2,(pr2 (REAL,{0})) #);