theorem :: FINSEQ_1:109

for A being included_in_Seg set
for B being set st B c= A holds
B is included_in_Seg by LL1;