let L be non empty reflexive antisymmetric RelStr ; for a being Element of L holds
( sup {a} = a & inf {a} = a )
let a be Element of L; ( sup {a} = a & inf {a} = a )
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
sup {a} = a
by A1, Th30; inf {a} = a
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
inf {a} = a
by A3, Th31; verum