let L be non empty up-complete Poset; :: thesis: ( L is finite implies for x being Element of L holds x is isolated_from_below )
assume A1: the carrier of L is finite ; :: according to STRUCT_0:def 11 :: thesis: for x being Element of L holds x is isolated_from_below
let x be Element of L; :: thesis: x is isolated_from_below
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 x <= sup D ; :: thesis: ex d being Element of L st
( d in D & x <= d )
hence ex d being Element of L st
( d in D & x <= d ) by A1, Th16; :: thesis: verum