let L be non empty antisymmetric upper-bounded RelStr ; :: thesis: ( ex_inf_of {} ,L & ex_sup_of the carrier of L,L )
consider a being Element of L such that
A1: a is_>=_than the carrier of L by Def5;
now :: thesis: ex a being Element of L st
( a is_<=_than {} & ( for b being Element of L st b is_<=_than {} holds
a >= b ) )
take a = a; :: thesis: ( a is_<=_than {} & ( for b being Element of L st b is_<=_than {} holds
a >= b ) )
thus a is_<=_than {} ; :: thesis: for b being Element of L st b is_<=_than {} holds
a >= b
thus for b being Element of L st b is_<=_than {} holds
a >= b by A1; :: thesis: verum
end;
hence ex_inf_of {} ,L by Th16; :: thesis: ex_sup_of the carrier of L,L
for b being Element of L st the carrier of L is_<=_than b holds
a <= b ;
hence ex_sup_of the carrier of L,L by A1, Th15; :: thesis: verum