deffunc H₁( Element of IIG) -> natural number = 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 number ; :: according to MEMBERED:def 6 :: thesis: ( not e in { H₁(v) where v is Element of IIG : v in the carrier of IIG } or 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;

consider v being Element of IIG;
A2: depth v,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;
take max Ds ; :: 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 } & max Ds = max Ds )
take Ds ; :: thesis: ( Ds = { (depth v,A) where v is Element of IIG : v in the carrier of IIG } & max Ds = max Ds )
thus ( Ds = { (depth v,A) where v is Element of IIG : v in the carrier of IIG } & max Ds = max Ds ) ; :: thesis: verum