:: deftheorem defines are_generators_of SPPOL_1:def 5 :
for f1, f2 being FinSequence of the carrier of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) holds
( f1,f2 are_generators_of P iff ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ) );