per cases ( n in m or n = m or m in n ) by ORDINAL1:14;
suppose A1: n in m ; :: thesis: n \/ m = max (n,m)
then A2: n \/ m = m by ORDINAL1:def 2, XBOOLE_1:12;
n in Segm m by A1;
hence n \/ m = max (n,m) by A2, NAT_1:44, XXREAL_0:def 10; :: thesis: verum
end;
suppose n = m ; :: thesis: n \/ m = max (n,m)
hence n \/ m = max (n,m) ; :: thesis: verum
end;
suppose A3: m in n ; :: thesis: n \/ m = max (n,m)
then A4: n \/ m = n by ORDINAL1:def 2, XBOOLE_1:12;
m in Segm n by A3;
hence n \/ m = max (n,m) by A4, NAT_1:44, XXREAL_0:def 10; :: thesis: verum
end;
end;