:: deftheorem Def7 defines depth CIRCUIT1:def 7 :
for IIG being non empty finite non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for b₃ being Nat holds
( b₃ = depth A iff 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 } & b₃ = max Ds ) );