let L1 be non empty up-complete Poset; :: thesis: ( L1 is finite implies for x being Element of L1 holds x in compactbelow x )
assume A1: L1 is finite ; :: thesis: for x being Element of L1 holds x in compactbelow x
let x be Element of L1; :: thesis: x in compactbelow x
A2: x <= x ;
x is compact by A1, WAYBEL_3:17;
hence x in compactbelow x by A2; :: thesis: verum