:: deftheorem defines is_alternative_in MIDSP_3:def 7 :
for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2 holds
( RAS is_alternative_in i iff for a being Point of RAS
for p being Tuple of (n + 1),RAS
for pii being Point of RAS st p . i = pii holds
*' (a,(p +* ((i + 1),pii))) = a );