let L be lower-bounded continuous LATTICE; :: thesis: L -waybelow is approximating
let x be Element of L; :: according to WAYBEL_4:def 17 :: thesis: x = sup ((L -waybelow) -below x)
x = sup (waybelow x) by WAYBEL_3:def 5;
hence x = sup ((L -waybelow) -below x) by Th40; :: thesis: verum