for A being set st A in rng M holds
A c= X
proof
let A be set ; :: thesis: ( A in rng M implies A c= X )
assume A1: A in rng M ; :: thesis: A c= X
rng M c= bool X by RELAT_1:def 19;
hence A c= X by A1; :: thesis: verum
end;
then union (rng M) c= X by ZFMISC_1:76;
hence Union M is Subset of X by CARD_3:def 4; :: thesis: verum