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 ) )
A1: 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 )
A2: b in {a,b} by TARSKI:def 2;
assume a0 is_>=_than {a,b} ; :: thesis: b <= a0
hence b <= a0 by A2, LATTICE3:def 9; :: thesis: verum
end;
A3: 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 )
A4: a in {a,b} by TARSKI:def 2;
assume a0 is_<=_than {a,b} ; :: thesis: a >= a0
hence a >= a0 by A4, LATTICE3:def 8; :: thesis: verum
end;
assume A5: a <= b ; :: thesis: ( sup {a,b} = b & inf {a,b} = a )
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 A5, TARSKI:def 2;
hence a0 >= a ; :: thesis: verum
end;
then for x being Element of R st x in {a,b} holds
x >= a ;
then A6: a is_<=_than {a,b} by LATTICE3:def 8;
for x being Element of R st x in {a,b} holds
x <= b by A5, TARSKI:def 2;
then b is_>=_than {a,b} by LATTICE3:def 9;
hence ( sup {a,b} = b & inf {a,b} = a ) by A6, A1, A3, YELLOW_0:30, YELLOW_0:31; :: thesis: verum