let L be non empty up-complete Poset; :: thesis: ( L is finite implies for x being Element of L holds x is compact )
assume A1: the carrier of L is finite ; :: according to STRUCT_0:def 11 :: thesis: for x being Element of L holds x is compact
let x be Element of L; :: thesis: x is compact
let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1,WAYBEL_3:def 2 :: thesis: ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
assume A2: x <= sup D ; :: thesis: ex d being Element of L st
( d in D & x <= d )
D is finite by A1;
hence ex d being Element of L st
( d in D & x <= d ) by A2, Th16; :: thesis: verum