let L be non empty reflexive antisymmetric RelStr ; for a being Element of L holds
( ex_sup_of {a},L & ex_inf_of {a},L )
let a be Element of L; ( 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; 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; verum