deffunc H₁( Element of ) -> Element of bool the carrier of L = downarrow $1;
A1: for x being Element of holds H₁(x) is Element of by Th43;
thus ex m being Function of L,(InclPoset (Ids L)) st
for x being Element of holds m . x = H₁(x) from FUNCT_2:sch 9(A1); :: thesis: verum