theorem Th3: :: WAYBEL14:3

for R being non empty transitive antisymmetric with_infima RelStr
for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)