set S = { i where i is Nat : p in LSeg (f,i) } ;

A2: { i where i is Nat : p in LSeg (f,i) } c= NAT

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 Nat : p in LSeg (f,i) } by A3;

then reconsider S = { i where i is 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 Nat : p in LSeg (f,i) } )

take S ; :: thesis: ( min S = min S & S = { i where i is Nat : p in LSeg (f,i) } )

thus ( min S = min S & S = { i where i is Nat : p in LSeg (f,i) } ) ; :: thesis: verum

A2: { i where i is Nat : p in LSeg (f,i) } c= NAT

proof

consider i2 being Nat such that
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { i where i is Nat : p in LSeg (f,i) } or x in NAT )

assume x in { i where i is Nat : p in LSeg (f,i) } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & p in LSeg (f,i) ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume x in { i where i is Nat : p in LSeg (f,i) } ; :: thesis: x in NAT

then ex i being Nat st

( x = i & p in LSeg (f,i) ) ;

hence x in NAT by ORDINAL1:def 12; :: thesis: verum

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 Nat : p in LSeg (f,i) } by A3;

then reconsider S = { i where i is 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 Nat : p in LSeg (f,i) } )

take S ; :: thesis: ( min S = min S & S = { i where i is Nat : p in LSeg (f,i) } )

thus ( min S = min S & S = { i where i is Nat : p in LSeg (f,i) } ) ; :: thesis: verum