let R, S be non empty reflexive transitive antisymmetric with_suprema RelStr ; 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; 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; ( 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
; 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;
( 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
;
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;
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; verum