set E = {{}};
take {{}} ; :: thesis: ( {{}} is n -at_most_dimensional & {{}} is subset-closed & not {{}} is empty )
thus ( {{}} is n -at_most_dimensional & {{}} is subset-closed & not {{}} is empty ) by Lm2; :: thesis: verum