let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; :: thesis: for x, y being Element of R
for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
let x, y be Element of R; :: thesis: for a, b being Element of S st the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b holds
x "\/" y = a "\/" b
let a, b be Element of S; :: thesis: ( the carrier of R /\ the carrier of S is directed lower Subset of S & the carrier of R /\ the carrier of S is upper Subset of R & R tolerates S & x = a & y = b implies x "\/" y = a "\/" b )
assume that
A1: the carrier of R /\ the carrier of S is directed lower Subset of S and
A2: the carrier of R /\ the carrier of S is upper Subset of R and
A3: R tolerates S and
A4: x = a and
A5: y = b ; :: thesis: x "\/" y = a "\/" b
( a in the carrier of R /\ the carrier of S & b in the carrier of R /\ the carrier of S ) by A4, A5, XBOOLE_0:def 4;
then reconsider xy = a "\/" b as Element of R by A1, Th13, Th16;
a "\/" b >= b by YELLOW_0:22;
then A6: xy >= y by A3, A5, Th15;
A7: for d being Element of R st d >= x & d >= y holds
xy <= d

proof

let d be Element of R; :: thesis: ( d >= x & d >= y implies xy <= d )
reconsider X = x, D = d as Element of (R [*] S) by Th10;
assume that
A8: d >= x and
A9: d >= y ; :: thesis: xy <= d
X <= D by A3, A8, Th8;
then reconsider dd = d as Element of S by A2, A4, Th18;
( dd >= a & b <= dd ) by A3, A4, A5, A8, A9, Th15;
then a "\/" b <= dd by YELLOW_5:9;
hence xy <= d by A3, Th15; :: thesis: verum

end;

a "\/" b >= a by YELLOW_0:22;
then xy >= x by A3, A4, Th15;
hence x "\/" y = a "\/" b by A6, A7, YELLOW_0:22; :: thesis: verum