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