theorem :: GROUP_9:123

for y being set
for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) by Lm38;