let A be non empty RelStr ; :: thesis: ( A is complete implies ( A is with_suprema & A is with_infima ) )
assume A1: for X being set ex a being Element of A st
( X is_<=_than a & ( for b being Element of A st X is_<=_than b holds
a <= b ) ) ; :: according to LATTICE3:def 12 :: thesis: ( A is with_suprema & A is with_infima )
thus A is with_suprema :: thesis: A is with_infima

proof

let a be Element of A; :: according to LATTICE3:def 10 :: thesis: for y being Element of A ex z being Element of A st
( a <= z & y <= z & ( for z' being Element of A st a <= z' & y <= z' holds
z <= z' ) )
let b be Element of A; :: thesis: ex z being Element of A st
( a <= z & b <= z & ( for z' being Element of A st a <= z' & b <= z' holds
z <= z' ) )
consider c being Element of A such that
A2: ( {a,b} is_<=_than c & ( for c' being Element of A st {a,b} is_<=_than c' holds
c <= c' ) ) by A1;
take c ; :: thesis: ( a <= c & b <= c & ( for z' being Element of A st a <= z' & b <= z' holds
c <= z' ) )
( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
hence ( a <= c & b <= c ) by A2, Def9; :: thesis: for z' being Element of A st a <= z' & b <= z' holds
c <= z'
let c' be Element of A; :: thesis: ( a <= c' & b <= c' implies c <= c' )
assume A3: ( a <= c' & b <= c' ) ; :: thesis: c <= c'
{a,b} is_<=_than c'

proof

let d be Element of A; :: according to LATTICE3:def 9 :: thesis: ( d in {a,b} implies d <= c' )
assume d in {a,b} ; :: thesis: d <= c'
hence d <= c' by A3, TARSKI:def 2; :: thesis: verum

end;

hence c <= c' by A2; :: thesis: verum

end;

let a be Element of A; :: according to LATTICE3:def 11 :: thesis: for y being Element of A ex z being Element of A st
( z <= a & z <= y & ( for z' being Element of A st z' <= a & z' <= y holds
z' <= z ) )
let b be Element of A; :: thesis: ex z being Element of A st
( z <= a & z <= b & ( for z' being Element of A st z' <= a & z' <= b holds
z' <= z ) )
set X = { c where c is Element of A : ( c <= a & c <= b ) } ;
consider c being Element of A such that
A4: ( { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c & ( for c' being Element of A st { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c' holds
c <= c' ) ) by A1;
take c ; :: thesis: ( c <= a & c <= b & ( for z' being Element of A st z' <= a & z' <= b holds
z' <= c ) )
{ c where c is Element of A : ( c <= a & c <= b ) } is_<=_than a

proof

let c be Element of A; :: according to LATTICE3:def 9 :: thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= a )
assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; :: thesis: c <= a
then ex c' being Element of A st
( c = c' & c' <= a & c' <= b ) ;
hence c <= a ; :: thesis: verum

end;

hence c <= a by A4; :: thesis: ( c <= b & ( for z' being Element of A st z' <= a & z' <= b holds
z' <= c ) )
{ c where c is Element of A : ( c <= a & c <= b ) } is_<=_than b

proof

let c be Element of A; :: according to LATTICE3:def 9 :: thesis: ( c in { c where c is Element of A : ( c <= a & c <= b ) } implies c <= b )
assume c in { c where c is Element of A : ( c <= a & c <= b ) } ; :: thesis: c <= b
then ex c' being Element of A st
( c = c' & c' <= a & c' <= b ) ;
hence c <= b ; :: thesis: verum

end;

hence c <= b by A4; :: thesis: for z' being Element of A st z' <= a & z' <= b holds
z' <= c
let c' be Element of A; :: thesis: ( c' <= a & c' <= b implies c' <= c )
assume ( c' <= a & c' <= b ) ; :: thesis: c' <= c
then c' in { c where c is Element of A : ( c <= a & c <= b ) } ;
hence c' <= c by A4, Def9; :: thesis: verum