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)
( {x} "\/" {y} = {(x "\/" y)} & (uparrow x) "\/" (uparrow y) c= uparrow ((uparrow x) "\/" (uparrow y)) ) by WAYBEL_0:16, YELLOW_4:19;
then A1: (uparrow x) "\/" (uparrow y) c= uparrow (x "\/" y) by YELLOW_4:35;
( wayabove x c= uparrow x & wayabove y c= uparrow y ) by WAYBEL_3:11;
then (wayabove x) "\/" (wayabove y) c= (uparrow x) "\/" (uparrow y) by YELLOW_4:21;
hence (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) by A1; :: thesis: verum