let S be ManySortedSign ; :: thesis: for X, Y being ManySortedSet of st X c= Y & X is with_missing_variables holds
Y is with_missing_variables
let X, Y be ManySortedSet of ; :: thesis: ( X c= Y & X is with_missing_variables implies Y is with_missing_variables )
assume that
A1: X c= Y and
A2: X " {{} } c= rng the ResultSort of S ; :: according to ABCMIZ_1:def 55 :: thesis: Y is with_missing_variables
let x be set ; :: according to TARSKI:def 3,ABCMIZ_1:def 55 :: thesis: ( not x in Y " {{} } or x in rng the ResultSort of S )
assume A3: x in Y " {{} } ; :: thesis: x in rng the ResultSort of S
then A4: x in dom Y by FUNCT_1:def 13;
A5: Y . x in {{} } by A3, FUNCT_1:def 13;
A6: dom Y = the carrier of S by PARTFUN1:def 4;
A7: dom X = the carrier of S by PARTFUN1:def 4;
A8: Y . x = {} by A5, TARSKI:def 1;
X . x c= Y . x by A1, A4, A6, PBOOLE:def 5;
then X . x = {} by A8;
then X . x in {{} } by TARSKI:def 1;
then x in X " {{} } by A4, A6, A7, FUNCT_1:def 13;
hence x in rng the ResultSort of S by A2; :: thesis: verum