per cases ( n >= m or m >= n ) ;

suppose A1: n >= m ; :: thesis: n \/ m = max (m,n)

then card (Segm m) c= card (Segm n) by NAT_1:40;
then m \/ n = n by XBOOLE_1:12;
hence n \/ m = max (m,n) by A1, XXREAL_0:def 10; :: thesis: verum

end;

suppose A1: m >= n ; :: thesis: n \/ m = max (m,n)

then card (Segm n) c= card (Segm m) by NAT_1:40;
then m \/ n = m by XBOOLE_1:12;
hence n \/ m = max (m,n) by A1, XXREAL_0:def 10; :: thesis: verum

end;

end;