A1: for d being Element of R st d >>= a & d >>= b holds
max (a,b) <<= d

proof

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;

max (a,b) >= b by XXREAL_0:25;
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