let R be with_infima Poset; :: thesis: for x, y being Element of R holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
let x, y be Element of R; :: thesis: (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
( {x} "/\" {y} = {(x "/\" y)} & (downarrow x) "/\" (downarrow y) c= downarrow ((downarrow x) "/\" (downarrow y)) ) by WAYBEL_0:16, YELLOW_4:46;
then A1: (downarrow x) "/\" (downarrow y) c= downarrow (x "/\" y) by YELLOW_4:62;
( waybelow x c= downarrow x & waybelow y c= downarrow y ) by WAYBEL_3:11;
then (waybelow x) "/\" (waybelow y) c= (downarrow x) "/\" (downarrow y) by YELLOW_4:48;
hence (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y) by A1; :: thesis: verum