let p, q be bag of n; :: thesis: ( ex k being Ordinal st
( p . k < q . k & ( for l being Ordinal st l in k holds
p . l = q . l ) ) implies for k being Ordinal holds
( not q . k < p . k or ex l being Ordinal st
( l in k & not q . l = p . l ) ) )
given k being Ordinal such that A1: p . k < q . k and
A2: for l being Ordinal st l in k holds
p . l = q . l ; :: thesis: for k being Ordinal holds
( not q . k < p . k or ex l being Ordinal st
( l in k & not q . l = p . l ) )
given k1 being Ordinal such that A3: q . k1 < p . k1 and
A4: for l being Ordinal st l in k1 holds
q . l = p . l ; :: thesis: contradiction

per cases ( k in k1 or k1 in k or k1 = k ) by ORDINAL1:14;

suppose k in k1 ; :: thesis: contradiction

hence contradiction by A1, A4; :: thesis: verum

end;

suppose k1 in k ; :: thesis: contradiction

hence contradiction by A2, A3; :: thesis: verum

end;

suppose k1 = k ; :: thesis: contradiction

hence contradiction by A1, A3; :: thesis: verum

end;

end;