theorem :: UNIALG_3:24

for U0 being strict with_const_op Universal_Algebra
for F being Function of the carrier of U0, the carrier of U0 st F = id the carrier of U0 holds
FuncLatt F = id the carrier of (UnSubAlLattice U0)