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