let n be Ordinal; :: thesis: BagOrder n is_reflexive_in Bags n
let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in Bags n or [x,x] in BagOrder n )
assume x in Bags n ; :: thesis: [x,x] in BagOrder n
then reconsider x' = x as bag of by Def14;
x' <=' x' ;
hence [x,x] in BagOrder n by Def16; :: thesis: verum