let n be Element of NAT ; :: thesis: for X being Subset of holds 2 (.) X c= X (+) X
let X be Subset of ; :: thesis: 2 (.) X c= X (+) X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 2 (.) X or x in X (+) X )
assume x in 2 (.) X ; :: thesis: x in X (+) X
then consider z being Point of such that
A1: x = 2 * z and
A2: z in X ;
x = (1 + 1) * z by A1
.= (1 * z) + (1 * z) by EUCLID:37
.= z + (1 * z) by EUCLID:33
.= z + z by EUCLID:33 ;
hence x in X (+) X by A2; :: thesis: verum