let I be set ; :: thesis: for M being RelExtension of finite-MultiSet_over I holds the carrier of M = Bags I
set N = finite-MultiSet_over I;
let M be RelExtension of finite-MultiSet_over I; :: thesis: the carrier of M = Bags I
thus the carrier of M c= Bags I :: according to XBOOLE_0:def 10 :: thesis: Bags I c= the carrier of M
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of M or a in Bags I )
assume a in the carrier of M ; :: thesis: a in Bags I
hence a in Bags I by PRE_POLY:def 12; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Bags I or a in the carrier of M )
assume a in Bags I ; :: thesis: a in the carrier of M
then a is bag of I by PRE_POLY:def 12;
then a is Element of (finite-MultiSet_over I) by Th1;
then a is Element of M by Th2;
hence a in the carrier of M ; :: thesis: verum