theorem Th7: :: FINSEQ_1:7

for a, c being natural Number st c <= a holds
Seg c = (Seg a) /\ (Seg c) by Th5, XBOOLE_1:28;