let R be with_suprema Poset; :: thesis: for x, y being Element of R holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
let x, y be Element of R; :: thesis: (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
( wayabove x c= uparrow x & wayabove y c= uparrow y ) by WAYBEL_3:11;
then A1: (wayabove x) "\/" (wayabove y) c= (uparrow x) "\/" (uparrow y) by YELLOW_4:21;
A2: {x} "\/" {y} = {(x "\/" y)} by YELLOW_4:19;
(uparrow x) "\/" (uparrow y) c= uparrow ((uparrow x) "\/" (uparrow y)) by WAYBEL_0:16;
then (uparrow x) "\/" (uparrow y) c= uparrow (x "\/" y) by A2, YELLOW_4:35;
hence (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) by A1, XBOOLE_1:1; :: thesis: verum