A1:
for d being Element of R st d >>= a & d >>= b holds

max (a,b) <<= d

then A2: max (a,b) >>= b by Th3;

max (a,b) >= a by XXREAL_0:25;

then max (a,b) >>= a by Th3;

hence a "\/" b = max (a,b) by A2, A1, YELLOW_0:22; :: thesis: verum

max (a,b) <<= d

proof

max (a,b) >= b
by XXREAL_0:25;
let d be Element of R; :: thesis: ( d >>= a & d >>= b implies max (a,b) <<= d )

assume ( d >>= a & d >>= b ) ; :: thesis: max (a,b) <<= d

then ( d >= a & d >= b ) by Th3;

then max (a,b) <= d by XXREAL_0:28;

hence max (a,b) <<= d by Th3; :: thesis: verum

end;assume ( d >>= a & d >>= b ) ; :: thesis: max (a,b) <<= d

then ( d >= a & d >= b ) by Th3;

then max (a,b) <= d by XXREAL_0:28;

hence max (a,b) <<= d by Th3; :: thesis: verum

then A2: max (a,b) >>= b by Th3;

max (a,b) >= a by XXREAL_0:25;

then max (a,b) >>= a by Th3;

hence a "\/" b = max (a,b) by A2, A1, YELLOW_0:22; :: thesis: verum