per cases ( n in m or n = m or m in n ) by ORDINAL1:14;

suppose A5: n in m ; :: thesis: n /\ m = min (n,m)

then A6: n /\ m = n by ORDINAL1:def 2, XBOOLE_1:28;
n in Segm m by A5;
hence n /\ m = min (n,m) by A6, NAT_1:44, XXREAL_0:def 9; :: thesis: verum

end;

suppose n = m ; :: thesis: n /\ m = min (n,m)

hence n /\ m = min (n,m) ; :: thesis: verum

end;

suppose A7: m in n ; :: thesis: n /\ m = min (n,m)

then A8: n /\ m = m by ORDINAL1:def 2, XBOOLE_1:28;
m in Segm n by A7;
hence n /\ m = min (n,m) by A8, NAT_1:44, XXREAL_0:def 9; :: thesis: verum

end;

end;