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
proof
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;
consider i2 being 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 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