theorem :: FINSEQ_1:8

for a, c being natural Number st Seg c = (Seg c) /\ (Seg a) holds
c <= a by Th6, Th7;