:: deftheorem defines -l> QUANTAL1:def 16 :
for Q being non empty QuantaleStr
for a, b being Element of Q holds a -l> b = "\/" ( { c where c is Element of Q : a [*] c [= b } ,Q);