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;

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 )

hence
P is algebraic
by WAYBEL_8:7; :: thesis: verumex 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;( 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