let X be integer-membered set ; :: thesis: ( ( for i being Integer holds i in X ) implies X = INT )
assume A1: for i being Integer holds i in X ; :: thesis: X = INT
thus X c= INT by Th5; :: according to XBOOLE_0:def 10 :: thesis: INT c= X
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in INT or e in X )
assume e in INT ; :: thesis: e in X
hence e in X by A1; :: thesis: verum