let a be Integer; :: thesis: for X being Subset of holds a ++ X c= INT
let X be Subset of ; :: thesis: a ++ X c= INT
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a ++ X or x in INT )
assume A1: x in a ++ X ; :: thesis: x in INT
then reconsider x' = x as Real ;
consider y being Real such that
A2: y in X and
A3: x' = a + y by A1, MEASURE6:def 6;
reconsider y' = y as Integer by A2;
x' = a + y' by A3;
hence x in INT by INT_1:def 2; :: thesis: verum