let L be non empty antisymmetric complete RelStr ; :: thesis: for X being set holds
( ex_sup_of X,L & ex_inf_of X,L )
let X be set ; :: thesis: ( ex_sup_of X,L & ex_inf_of X,L )
set Y = { c where c is Element of L : c is_<=_than X } ;
consider a being Element of L such that
A1: { c where c is Element of L : c is_<=_than X } is_<=_than a and
A2: for b being Element of L st { c where c is Element of L : c is_<=_than X } is_<=_than b holds
a <= b by LATTICE3:def 12;
ex a being Element of L st
( X is_<=_than a & ( for b being Element of L st X is_<=_than b holds
a <= b ) ) by LATTICE3:def 12;
hence ex_sup_of X,L by Th15; :: thesis: ex_inf_of X,L
now :: thesis: ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) )
take a = a; :: thesis: ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) )
thus a is_<=_than X :: thesis: for b being Element of L st b is_<=_than X holds
b <= a
proof
let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in X or a <= b )
assume A3: b in X ; :: thesis: a <= b
{ c where c is Element of L : c is_<=_than X } is_<=_than b
proof
let c be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not c in { c where c is Element of L : c is_<=_than X } or c <= b )
assume c in { c where c is Element of L : c is_<=_than X } ; :: thesis: c <= b
then ex d being Element of L st
( c = d & d is_<=_than X ) ;
hence c <= b by A3; :: thesis: verum
end;
hence a <= b by A2; :: thesis: verum
end;
let b be Element of L; :: thesis: ( b is_<=_than X implies b <= a )
assume b is_<=_than X ; :: thesis: b <= a
then b in { c where c is Element of L : c is_<=_than X } ;
hence b <= a by A1; :: thesis: verum
end;
hence ex_inf_of X,L by Th16; :: thesis: verum