let n be Nat; :: thesis: {{}} is n -at_most_dimensional
set E = {{}};
thus {{}} is n -at_most_dimensional :: thesis: verum

proof

let x be set ; :: according to SCMYCIEL:def 4 :: thesis: ( x in {{}} implies card x c= n + 1 )
assume x in {{}} ; :: thesis: card x c= n + 1
then x = {} by TARSKI:def 1;
hence card x c= n + 1 ; :: thesis: verum

end;