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
proof
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 }
proof
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;
hence x <= y by A3; :: thesis: verum
end;
let y be Element of L; :: thesis: ( y is_<=_than X implies 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