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

take a = a; :: thesis: ( a is_>=_than {} & ( for b being Element of L st b is_>=_than {} holds
a <= b ) )
thus a is_>=_than {} by Th6; :: 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, LATTICE3:def 8; :: 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 by LATTICE3:def 8;
hence ex_inf_of the carrier of L,L by A1, Th16; :: thesis: verum