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