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 st
( X is_<=_than a & ( for b being Element of 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 ; :: according to LATTICE3:def 10 :: thesis: for y being Element of ex z being Element of st
( a <= z & y <= z & ( for z' being Element of st a <= z' & y <= z' holds
z <= z' ) )
let b be Element of ; :: thesis: ex z being Element of st
( a <= z & b <= z & ( for z' being Element of st a <= z' & b <= z' holds
z <= z' ) )
consider c being Element of such that
A2: {a,b} is_<=_than c and
A3: for c' being Element of st {a,b} is_<=_than c' holds
c <= c' by A1;
take c ; :: thesis: ( a <= c & b <= c & ( for z' being Element of st a <= z' & b <= z' holds
c <= z' ) )
A4: a in {a,b} by TARSKI:def 2;
b in {a,b} by TARSKI:def 2;
hence ( a <= c & b <= c ) by A2, A4, Def9; :: thesis: for z' being Element of st a <= z' & b <= z' holds
c <= z'
let c' be Element of ; :: thesis: ( a <= c' & b <= c' implies c <= c' )
assume that
A5: a <= c' and
A6: b <= c' ; :: thesis: c <= c'
{a,b} is_<=_than c'

proof

let d be Element of ; :: 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 A5, A6, TARSKI:def 2; :: thesis: verum

end;

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

end;

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

proof

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

end;

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

proof

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

end;

hence c <= b by A8; :: thesis: for z' being Element of st z' <= a & z' <= b holds
z' <= c
let c' be Element of ; :: thesis: ( c' <= a & c' <= b implies c' <= c )
assume that
A9: c' <= a and
A10: c' <= b ; :: thesis: c' <= c
c' in { c where c is Element of : ( c <= a & c <= b ) } by A9, A10;
hence c' <= c by A7, Def9; :: thesis: verum