theorem Th1: :: FINSEQ_2:2

for i, j, l being natural Number st l = min (i,j) holds
(Seg i) /\ (Seg j) = Seg l