let P be non empty upper-bounded Poset; :: thesis: ( the InternalRel of P is well-ordering implies P is algebraic )
assume A1: the InternalRel of P is well-ordering ; :: thesis: P is algebraic
then reconsider L = P as non empty complete connected continuous Poset by Th9;

now :: thesis: for x, y being Element of L st x << y holds
ex z being Element of L st
( z in the carrier of (CompactSublatt L) & x <= z & z <= y )

let x, y be Element of L; :: thesis: ( x << y implies ex z being Element of L st
( z in the carrier of (CompactSublatt L) & x <= z & z <= y ) )
assume x << y ; :: thesis: ex z being Element of L st
( z in the carrier of (CompactSublatt L) & x <= z & z <= y )
then ( ( x is compact & x <= x & x <= y ) or x < y ) by WAYBEL_3:1;
then consider z being Element of L such that
A2: z is compact and
A3: ( x <= z & z <= y ) by A1, Th10;
take z = z; :: thesis: ( z in the carrier of (CompactSublatt L) & x <= z & z <= y )
thus z in the carrier of (CompactSublatt L) by A2, WAYBEL_8:def 1; :: thesis: ( x <= z & z <= y )
thus ( x <= z & z <= y ) by A3; :: thesis: verum

end;

hence P is algebraic by WAYBEL_8:7; :: thesis: verum