theorem Th13: :: QUANTAL1:13

for Q being Quantale
for s, a, b being Element of Q st a [= b holds
( b -r> s [= a -r> s & b -l> s [= a -l> s )