theorem Th57: :: MATRIX13:57

for D being non empty set
for A being Matrix of D
for P, P1, Q, Q1 being finite without_zero Subset of NAT holds
not ( ( P = {} implies Q = {} ) & ( Q = {} implies P = {} ) & [:P,Q:] c= Indices (Segm (A,P1,Q1)) & ( for P2, Q2 being finite without_zero Subset of NAT holds
( not P2 c= P1 or not Q2 c= Q1 or not P2 = (Sgm P1) .: P or not Q2 = (Sgm Q1) .: Q or not card P2 = card P or not card Q2 = card Q or not Segm ((Segm (A,P1,Q1)),P,Q) = Segm (A,P2,Q2) ) ) )