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 z9 being Element of A st a <= z9 & y <= z9 holds
z <= z9 ) )
let b be Element of A; :: thesis: ex z being Element of A st
( a <= z & b <= z & ( for z9 being Element of A st a <= z9 & b <= z9 holds
z <= z9 ) )
consider c being Element of A such that
A2: {a,b} is_<=_than c and
A3: for c9 being Element of A st {a,b} is_<=_than c9 holds
c <= c9 by A1;
take c ; :: thesis: ( a <= c & b <= c & ( for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9 ) )
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; :: thesis: for z9 being Element of A st a <= z9 & b <= z9 holds
c <= z9
let c9 be Element of A; :: thesis: ( a <= c9 & b <= c9 implies c <= c9 )
assume that
A5: a <= c9 and
A6: b <= c9 ; :: thesis: c <= c9
{a,b} is_<=_than c9 by A5, A6, TARSKI:def 2;
hence c <= c9 by A3; :: 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 z9 being Element of A st z9 <= a & z9 <= y holds
z9 <= z ) )
let b be Element of A; :: thesis: ex z being Element of A st
( z <= a & z <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= z ) )
set X = { c where c is Element of A : ( c <= a & c <= b ) } ;
consider c being Element of A such that
A7: { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c and
A8: for c9 being Element of A st { c where c is Element of A : ( c <= a & c <= b ) } is_<=_than c9 holds
c <= c9 by A1;
take c ; :: thesis: ( c <= a & c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= 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 c9 being Element of A st
( c = c9 & c9 <= a & c9 <= b ) ;
hence c <= a ; :: thesis: verum
end;
hence c <= a by A8; :: thesis: ( c <= b & ( for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= 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 c9 being Element of A st
( c = c9 & c9 <= a & c9 <= b ) ;
hence c <= b ; :: thesis: verum
end;
hence c <= b by A8; :: thesis: for z9 being Element of A st z9 <= a & z9 <= b holds
z9 <= c
let c9 be Element of A; :: thesis: ( c9 <= a & c9 <= b implies c9 <= c )
assume that
A9: c9 <= a and
A10: c9 <= b ; :: thesis: c9 <= c
c9 in { c where c is Element of A : ( c <= a & c <= b ) } by A9, A10;
hence c9 <= c by A7; :: thesis: verum