let n be Ordinal; :: thesis: for p, q being bag of n holds
( p <=' q or q <=' p )
let p, q be bag of n; :: thesis: ( p <=' q or q <=' p )
assume A1: not p <=' q ; :: thesis: q <=' p
then consider i being object such that
A2: i in n and
A3: p . i <> q . i by PBOOLE:3;
A4: not p < q by A1;
defpred S₁[ set ] means p . $1 <> q . $1;
A5: ex i being Ordinal st S₁[i] by A2, A3;
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:5;

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 A4, A8; :: thesis: verum

end;

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

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

end;

end;