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 () & 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 () & x <= z & z <= y ) )

assume x << y ; :: thesis: ex z being Element of L st
( z in the carrier of () & 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 ;
take z = z; :: thesis: ( z in the carrier of () & x <= z & z <= y )
thus z in the carrier of () by ; :: 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