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