let n be Ordinal; :: thesis: for T being TermOrder of n
for b being set st b in field T holds
b is bag of n
let T be TermOrder of n; :: thesis: for b being set st b in field T holds
b is bag of n
let b be set ; :: thesis: ( b in field T implies b is bag of n )
assume b in field T ; :: thesis: b is bag of n
then A1: b in (dom T) \/ (rng T) by RELAT_1:def 6;

per cases ( b in dom T or b in rng T ) by A1, XBOOLE_0:def 3;

suppose b in dom T ; :: thesis: b is bag of n

then b is Element of Bags n ;
hence b is bag of n ; :: thesis: verum

end;

suppose b in rng T ; :: thesis: b is bag of n

then b is Element of Bags n ;
hence b is bag of n ; :: thesis: verum

end;

end;