set S = { i where i is Element of NAT : p in LSeg (f,i) } ;
A2: { i where i is Element of NAT : p in LSeg (f,i) } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Element of NAT : p in LSeg (f,i) } or x in NAT )
assume x in { i where i is Element of NAT : p in LSeg (f,i) } ; :: thesis: x in NAT
then ex i being Element of NAT st
( x = i & p in LSeg (f,i) ) ;
hence x in NAT ; :: thesis: verum

end;

consider i2 being Element of NAT such that
1 <= i2 and
i2 + 1 <= len f and
A3: p in LSeg (f,i2) by A1, SPPOL_2:13;
i2 in { i where i is Element of NAT : p in LSeg (f,i) } by A3;
then reconsider S = { i where i is Element of NAT : p in LSeg (f,i) } as non empty Subset of NAT by A2;
take min S ; :: thesis: ex S being non empty Subset of NAT st
( min S = min S & S = { i where i is Element of NAT : p in LSeg (f,i) } )
take S ; :: thesis: ( min S = min S & S = { i where i is Element of NAT : p in LSeg (f,i) } )
thus ( min S = min S & S = { i where i is Element of NAT : p in LSeg (f,i) } ) ; :: thesis: verum