let L1 be non empty complete Poset; :: thesis: for x being Element of L1 st x is compact holds
x = inf (wayabove x)
let x be Element of L1; :: thesis: ( x is compact implies x = inf (wayabove x) )
assume x is compact ; :: thesis: x = inf (wayabove x)
then x << x by WAYBEL_3:def 2;
then x in wayabove x by WAYBEL_3:8;
then A1: inf (wayabove x) <= x by YELLOW_2:22;
x <= inf (wayabove x) by WAYBEL14:9;
hence x = inf (wayabove x) by A1, YELLOW_0:def 3; :: thesis: verum