for L being non empty RelStr
for x being Element of [:L,L:] holds (sup_op L) . x = (x `1) "\/" (x `2)