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