let L be non empty antisymmetric lower-bounded RelStr ; :: thesis: ( ex_sup_of {} ,L & ex_inf_of the carrier of L,L )
consider a being Element of L such that
A1: a is_<=_than the carrier of L by Def4;

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_sup_of {} ,L by Th15; :: thesis: ex_inf_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_inf_of the carrier of L,L by A1, Th16; :: thesis: verum