set X1 = {(0. X)};
reconsider X1 = {(0. X)} as Ideal of X by Lm3;
take X1 ; :: thesis: X1 is closed
for x being Element of X1 holds x ` in X1 by Lm4;
hence X1 is closed ; :: thesis: verum