:: deftheorem defines Ros LATTBA_1:def 11 :
for L being B_Lattice
for a, b, c being Element of L holds Ros (a,b,c) = ((a "/\" b) "\/" (b "/\" c)) "\/" (c "/\" a);