:: deftheorem defines first-line-of-anti-circular MATRIX16:def 11 :
for K being Field
for p being FinSequence of K holds
( p is first-line-of-anti-circular iff ex M being Matrix of len p,K st M is_anti-circular_about p );