:: deftheorem Def1 defines Cage JORDAN9:def 1 :
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st C is connected holds
for b₃ being non constant standard clockwise_oriented special_circular_sequence holds
( b₃ = Cage (C,n) iff ( b₃ is_sequence_on Gauge (C,n) & ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge (C,n)) & b₃ /. 1 = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) & b₃ /. 2 = (Gauge (C,n)) * ((i + 1),(width (Gauge (C,n)))) & N-min C in cell ((Gauge (C,n)),i,((width (Gauge (C,n))) -' 1)) & N-min C <> (Gauge (C,n)) * (i,((width (Gauge (C,n))) -' 1)) ) & ( for k being Nat st 1 <= k & k + 2 <= len b₃ holds
( ( front_left_cell (b₃,k,(Gauge (C,n))) misses C & front_right_cell (b₃,k,(Gauge (C,n))) misses C implies b₃ turns_right k, Gauge (C,n) ) & ( front_left_cell (b₃,k,(Gauge (C,n))) misses C & front_right_cell (b₃,k,(Gauge (C,n))) meets C implies b₃ goes_straight k, Gauge (C,n) ) & ( front_left_cell (b₃,k,(Gauge (C,n))) meets C implies b₃ turns_left k, Gauge (C,n) ) ) ) ) );