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

now

let z be set ; :: thesis: ( ( z in uparrow (x "\/" y) implies z in (uparrow x) /\ (uparrow y) ) & ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) ) )

hereby :: thesis: ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) )

assume A1: z in uparrow (x "\/" y) ; :: thesis: z in (uparrow x) /\ (uparrow y)
then reconsider z' = z as Element of ;
A2: z' >= x "\/" y by A1, WAYBEL_0:18;
x "\/" y >= y by YELLOW_0:22;
then z' >= y by A2, YELLOW_0:def 2;
then A3: z' in uparrow y by WAYBEL_0:18;
x "\/" y >= x by YELLOW_0:22;
then z' >= x by A2, YELLOW_0:def 2;
then z' in uparrow x by WAYBEL_0:18;
hence z in (uparrow x) /\ (uparrow y) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: z in (uparrow x) /\ (uparrow y) ; :: thesis: z in uparrow (x "\/" y)
then reconsider z' = z as Element of ;
z in uparrow y by A4, XBOOLE_0:def 4;
then A5: z' >= y by WAYBEL_0:18;
z in uparrow x by A4, XBOOLE_0:def 4;
then z' >= x by WAYBEL_0:18;
then x "\/" y <= z' by A5, YELLOW_0:22;
hence z in uparrow (x "\/" y) by WAYBEL_0:18; :: thesis: verum

end;

hence uparrow (x "\/" y) = (uparrow x) /\ (uparrow y) by TARSKI:2; :: thesis: verum