let R be non empty reflexive antisymmetric RelStr ; :: thesis: for x, y being Element of R st x <= y holds
( sup {x,y} = y & inf {x,y} = x )
let a, b be Element of R; :: thesis: ( a <= b implies ( sup {a,b} = b & inf {a,b} = a ) )
assume A1: a <= b ; :: thesis: ( sup {a,b} = b & inf {a,b} = a )
A2: b is_>=_than {a,b}

proof

for x being Element of R st x in {a,b} holds
x <= b by A1, TARSKI:def 2;
hence b is_>=_than {a,b} by LATTICE3:def 9; :: thesis: verum

end;

A3: a is_<=_than {a,b}

proof

for x being Element of {a,b} holds x >= a

proof

let a0 be Element of {a,b}; :: thesis: a0 >= a
( a <= a0 or a <= a0 ) by A1, TARSKI:def 2;
hence a0 >= a ; :: thesis: verum

end;

then for x being Element of R st x in {a,b} holds
x >= a ;
hence a is_<=_than {a,b} by LATTICE3:def 8; :: thesis: verum

end;

A4: for x being Element of R st x is_>=_than {a,b} holds
b <= x

proof

let a0 be Element of R; :: thesis: ( a0 is_>=_than {a,b} implies b <= a0 )
assume A5: a0 is_>=_than {a,b} ; :: thesis: b <= a0
( a0 >= a & a0 >= b )

proof

A6: a in {a,b} by TARSKI:def 2;
b in {a,b} by TARSKI:def 2;
hence ( a0 >= a & a0 >= b ) by A5, A6, LATTICE3:def 9; :: thesis: verum

end;

hence b <= a0 ; :: thesis: verum

end;

for x being Element of R st x is_<=_than {a,b} holds
a >= x

proof

let a0 be Element of R; :: thesis: ( a0 is_<=_than {a,b} implies a >= a0 )
assume A7: a0 is_<=_than {a,b} ; :: thesis: a >= a0
( a0 <= a & a0 <= b )

proof

A8: a in {a,b} by TARSKI:def 2;
b in {a,b} by TARSKI:def 2;
hence ( a0 <= a & a0 <= b ) by A7, A8, LATTICE3:def 8; :: thesis: verum

end;

hence a >= a0 ; :: thesis: verum

end;

hence ( sup {a,b} = b & inf {a,b} = a ) by A2, A3, A4, YELLOW_0:30, YELLOW_0:31; :: thesis: verum