let L be non empty reflexive antisymmetric RelStr ; :: thesis: for a being Element of L holds
( ex_sup_of {a},L & ex_inf_of {a},L )
let a be Element of L; :: thesis: ( ex_sup_of {a},L & ex_inf_of {a},L )
a <= a ;
then A1: ( a is_<=_than {a} & a is_>=_than {a} ) by Th7;
for b being Element of L st b is_>=_than {a} holds
b >= a by Th7;
hence ex_sup_of {a},L by A1, Th15; :: thesis: ex_inf_of {a},L
for b being Element of L st b is_<=_than {a} holds
b <= a by Th7;
hence ex_inf_of {a},L by A1, Th16; :: thesis: verum