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 A1: ( x in Bags n & y in Bags n & [x,y] in BagOrder n & [y,x] in BagOrder n ) ; :: thesis: x = y
then reconsider b1 = x, b2 = y as bag of by Def14;
A2: b1 <=' b2 by A1, Def16;
reconsider b1' = y, b2' = x as bag of by A1, Def14;
b1' <=' b2' by A1, Def16;
then ( ( b1 < b2 or b1 = b2 ) & ( b1' < b2' or b1' = b2' ) ) by A2, Def12;
hence x = y ; :: thesis: verum