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;