let L be non empty reflexive RelStr ; :: thesis: ( L is complete implies ( L is up-complete & L is /\-complete ) )

assume A1: L is complete ; :: thesis: ( L is up-complete & L is /\-complete )

thus L is up-complete by A1; :: thesis: L is /\-complete

let X be non empty Subset of L; :: according to WAYBEL_0:def 40 :: thesis: ex x being Element of L st

( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds

x >= y ) )

set Y = { y where y is Element of L : y is_<=_than X } ;

consider x being Element of L such that

A2: { y where y is Element of L : y is_<=_than X } is_<=_than x and

A3: for b being Element of L st { y where y is Element of L : y is_<=_than X } is_<=_than b holds

x <= b by A1;

take x ; :: thesis: ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds

x >= y ) )

thus x is_<=_than X :: thesis: for y being Element of L st y is_<=_than X holds

x >= y

assume y is_<=_than X ; :: thesis: x >= y

then y in { y where y is Element of L : y is_<=_than X } ;

hence x >= y by A2; :: thesis: verum

assume A1: L is complete ; :: thesis: ( L is up-complete & L is /\-complete )

thus L is up-complete by A1; :: thesis: L is /\-complete

let X be non empty Subset of L; :: according to WAYBEL_0:def 40 :: thesis: ex x being Element of L st

( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds

x >= y ) )

set Y = { y where y is Element of L : y is_<=_than X } ;

consider x being Element of L such that

A2: { y where y is Element of L : y is_<=_than X } is_<=_than x and

A3: for b being Element of L st { y where y is Element of L : y is_<=_than X } is_<=_than b holds

x <= b by A1;

take x ; :: thesis: ( x is_<=_than X & ( for y being Element of L st y is_<=_than X holds

x >= y ) )

thus x is_<=_than X :: thesis: for y being Element of L st y is_<=_than X holds

x >= y

proof

let y be Element of L; :: thesis: ( y is_<=_than X implies x >= y )
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in X or x <= y )

assume A4: y in X ; :: thesis: x <= y

y is_>=_than { y where y is Element of L : y is_<=_than X }

end;assume A4: y in X ; :: thesis: x <= y

y is_>=_than { y where y is Element of L : y is_<=_than X }

proof

hence
x <= y
by A3; :: thesis: verum
let z be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not z in { y where y is Element of L : y is_<=_than X } or z <= y )

assume z in { y where y is Element of L : y is_<=_than X } ; :: thesis: z <= y

then ex a being Element of L st

( z = a & a is_<=_than X ) ;

hence z <= y by A4; :: thesis: verum

end;assume z in { y where y is Element of L : y is_<=_than X } ; :: thesis: z <= y

then ex a being Element of L st

( z = a & a is_<=_than X ) ;

hence z <= y by A4; :: thesis: verum

assume y is_<=_than X ; :: thesis: x >= y

then y in { y where y is Element of L : y is_<=_than X } ;

hence x >= y by A2; :: thesis: verum