set T = TrivialInfiniteTree ;
let n be Nat; :: thesis: TrivialInfiniteTree -level n = {(n |-> 0)}
set L = { w where w is Element of TrivialInfiniteTree : len w = n } ;
set f = n |-> 0;
{(n |-> 0)} = { w where w is Element of TrivialInfiniteTree : len w = n }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { w where w is Element of TrivialInfiniteTree : len w = n } c= {(n |-> 0)}

let a be object ; :: thesis: ( a in {(n |-> 0)} implies a in { w where w is Element of TrivialInfiniteTree : len w = n } )
assume a in {(n |-> 0)} ; :: thesis: a in { w where w is Element of TrivialInfiniteTree : len w = n }
then A1: a = n |-> 0 by TARSKI:def 1;
( n |-> 0 in TrivialInfiniteTree & len (n |-> 0) = n ) by CARD_1:def 7;
hence a in { w where w is Element of TrivialInfiniteTree : len w = n } by A1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { w where w is Element of TrivialInfiniteTree : len w = n } or a in {(n |-> 0)} )
assume a in { w where w is Element of TrivialInfiniteTree : len w = n } ; :: thesis: a in {(n |-> 0)}
then consider w being Element of TrivialInfiniteTree such that
A2: ( a = w & len w = n ) ;
w in TrivialInfiniteTree ;
then ex k being Nat st w = k |-> 0 ;
then a = n |-> 0 by A2, CARD_1:def 7;
hence a in {(n |-> 0)} by TARSKI:def 1; :: thesis: verum

end;

hence TrivialInfiniteTree -level n = {(n |-> 0)} ; :: thesis: verum