let n be Ordinal; :: thesis: for p, q being bag of holds
( p <=' q or q <=' p )
let p, q be bag of ; :: thesis: ( p <=' q or q <=' p )
assume A1: not p <=' q ; :: thesis: q <=' p
then A2: ( not p < q & not p = q ) by Def12;
consider i being set such that
A3: i in n and
A4: p . i <> q . i by A1, PBOOLE:3;
reconsider j = i as Ordinal by A3;
defpred S₁[ set ] means p . $1 <> q . $1;
j in n by A3;
then A5: ex i being Ordinal st S₁[i] by A4;
consider m being Ordinal such that
A6: S₁[m] and
A7: for n being Ordinal st S₁[n] holds
m c= n from ORDINAL1:sch 1(A5);
A8: for l being Ordinal st l in m holds
q . l = p . l by A7, ORDINAL1:7;

per cases ( p . m < q . m or p . m > q . m ) by A6, XXREAL_0:1;

suppose p . m < q . m ; :: thesis: q <=' p

hence q <=' p by A2, A8, Def11; :: thesis: verum

end;

suppose p . m > q . m ; :: thesis: q <=' p

then q < p by A8, Def11;
hence q <=' p by Def12; :: thesis: verum

end;

end;