deffunc H₁( Element of IIG) -> Nat = depth ($1,A);
set Ds = { H₁(v) where v is Element of IIG : v in the carrier of IIG } ;
A1: { H₁(v) where v is Element of IIG : v in the carrier of IIG } is natural-membered

proof

let e be object ; :: according to MEMBERED:def 6 :: thesis: ( not e in { H₁(v) where v is Element of IIG : v in the carrier of IIG } or not e is natural )
assume e in { H₁(v) where v is Element of IIG : v in the carrier of IIG } ; :: thesis: e is natural
then ex v being Element of IIG st
( e = depth (v,A) & v in the carrier of IIG ) ;
hence e is natural ; :: thesis: verum

end;

set v = the Element of IIG;
A2: depth ( the Element of IIG,A) in { H₁(v) where v is Element of IIG : v in the carrier of IIG } ;
A3: the carrier of IIG is finite ;
{ H₁(v) where v is Element of IIG : v in the carrier of IIG } is finite from FRAENKEL:sch 21(A3);
then reconsider Ds = { H₁(v) where v is Element of IIG : v in the carrier of IIG } as non empty finite Subset of NAT by A1, A2, MEMBERED:6;
reconsider m = max Ds as Nat by TARSKI:1;
take m ; :: thesis: ex Ds being non empty finite Subset of NAT st
( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds )
take Ds ; :: thesis: ( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds )
thus ( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & m = max Ds ) ; :: thesis: verum