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

now :: thesis: for z being object holds
( ( z in uparrow (x "\/" y) implies z in (uparrow x) /\ (uparrow y) ) & ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) ) )

let z be object ; :: 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 z9 = z as Element of R ;
A2: z9 >= x "\/" y by A1, WAYBEL_0:18;
x "\/" y >= y by YELLOW_0:22;
then z9 >= y by A2, YELLOW_0:def 2;
then A3: z9 in uparrow y by WAYBEL_0:18;
x "\/" y >= x by YELLOW_0:22;
then z9 >= x by A2, YELLOW_0:def 2;
then z9 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 z9 = z as Element of R ;
z in uparrow y by A4, XBOOLE_0:def 4;
then A5: z9 >= y by WAYBEL_0:18;
z in uparrow x by A4, XBOOLE_0:def 4;
then z9 >= x by WAYBEL_0:18;
then x "\/" y <= z9 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