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