theorem :: SPPOL_1:38

for i being Nat
for P being Subset of (TOP-REAL 2)
for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds
f1 /. i is_extremal_in P