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 x9 = x as bag of n ;
x9 <=' x9 ;
hence [x,x] in BagOrder n by Def14; :: thesis: verum