let i, j, l be natural Number ; :: thesis: ( l = min (i,j) implies (Seg i) /\ (Seg j) = Seg l )
( i <= j or j <= i ) ;
then ( ( i <= j & (Seg i) /\ (Seg j) = Seg i ) or ( j <= i & (Seg i) /\ (Seg j) = Seg j ) ) by FINSEQ_1:7;
hence ( l = min (i,j) implies (Seg i) /\ (Seg j) = Seg l ) by XXREAL_0:def 9; :: thesis: verum