deffunc H₁( Element of NAT ) -> Element of bool the carrier of (TOP-REAL 2) = Lower_Arc (L~ (Cage (C,$1)));
thus ex S being SetSequence of the carrier of (TOP-REAL 2) st
for i being Element of NAT holds S . i = H₁(i) from FUNCT_2:sch 4(); :: thesis: verum