let R be non empty reflexive antisymmetric complete RelStr ; :: thesis: for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )
let x be Element of R; :: thesis: ( sup (waybelow x) <= x & x <= inf (wayabove x) )
x is_>=_than waybelow x by WAYBEL_3:9;
hence sup (waybelow x) <= x by YELLOW_0:32; :: thesis: x <= inf (wayabove x)
x is_<=_than wayabove x by WAYBEL_3:10;
hence x <= inf (wayabove x) by YELLOW_0:33; :: thesis: verum