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 )
A1: for b being Element of L st b is_>=_than {a} holds
b >= a by Th7;
A2: a <= a ;
then a is_>=_than {a} by Th7;
hence ex_sup_of {a},L by A1, Th15; :: thesis: ex_inf_of {a},L
A3: for b being Element of L st b is_<=_than {a} holds
b <= a by Th7;
a is_<=_than {a} by A2, Th7;
hence ex_inf_of {a},L by A3, Th16; :: thesis: verum