:: deftheorem RosTrnDef defines RosTrn LATTBA_1:def 12 :
for B being B_Lattice
for b₂ being TriOp of the carrier of B holds
( b₂ = RosTrn B iff for a, b, c being Element of B holds b₂ . (a,b,c) = Ros (a,b,c) );