for X being Subset of REAL holds X = 0 ++ X by MEMBER_1:146;