let a be Integer; :: thesis: for X being Subset of INT holds a ++ X c= INT

let X be Subset of INT; :: thesis: a ++ X c= INT

let x be object ; :: 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 x9 = x as Real ;

consider y being Complex such that

A2: x9 = a + y and

A3: y in X by A1, MEMBER_1:143;

reconsider y9 = y as Integer by A3;

x9 = a + y9 by A2;

hence x in INT by INT_1:def 2; :: thesis: verum

let X be Subset of INT; :: thesis: a ++ X c= INT

let x be object ; :: 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 x9 = x as Real ;

consider y being Complex such that

A2: x9 = a + y and

A3: y in X by A1, MEMBER_1:143;

reconsider y9 = y as Integer by A3;

x9 = a + y9 by A2;

hence x in INT by INT_1:def 2; :: thesis: verum