let n be Ordinal; :: thesis: BagOrder n is_antisymmetric_in Bags n
set BO = BagOrder n;
let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in Bags n or not y in Bags n or not [x,y] in BagOrder n or not [y,x] in BagOrder n or x = y )
assume that
A1: ( x in Bags n & y in Bags n ) and
A2: [x,y] in BagOrder n and
A3: [y,x] in BagOrder n ; :: thesis: x = y
reconsider b1 = x, b2 = y as bag of n by A1;
b1 <=' b2 by A2, Def16;
then A4: ( b1 < b2 or b1 = b2 ) by Def12;
reconsider b19 = y, b29 = x as bag of n by A1;
b19 <=' b29 by A3, Def16;
hence x = y by A4, Def12; :: thesis: verum