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 A1: ( 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 ) ; :: thesis: x "\/" y = a "\/" b
then ( a in the carrier of R /\ the carrier of S & b in the carrier of R /\ the carrier of S ) by XBOOLE_0:def 4;
then reconsider xy = a "\/" b as Element of R by A1, Th13, Th16;
a "\/" b >= a by YELLOW_0:22;
then A2: xy >= x by A1, Th15;
a "\/" b >= b by YELLOW_0:22;
then A3: xy >= y by A1, Th15;
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 )
assume A4: ( d >= x & d >= y ) ; :: thesis: xy <= d
reconsider X = x, D = d as Element of (R [*] S) by Th10;
X <= D by A1, A4, Th8;
then reconsider dd = d as Element of S by A1, Th18;
A5: dd >= a by A1, A4, Th15;
b <= dd by A1, A4, Th15;
then a "\/" b <= dd by A5, YELLOW_5:9;
hence xy <= d by A1, Th15; :: thesis: verum

end;

hence x "\/" y = a "\/" b by A2, A3, YELLOW_0:22; :: thesis: verum