let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty Circuit of IIG
for v being Vertex of IIG holds depth (v,A) <= depth A
let A be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG holds depth (v,A) <= depth A
let v be Vertex of IIG; :: thesis: depth (v,A) <= depth A
consider Ds being non empty finite Subset of NAT such that
A1: Ds = { (depth (v9,A)) where v9 is Element of IIG : v9 in the carrier of IIG } and
A2: depth A = max Ds by Def7;
reconsider Y = Ds as non empty finite real-membered set ;
depth (v,A) in Y by A1;
hence depth (v,A) <= depth A by A2, XXREAL_2:def 8; :: thesis: verum