deffunc H₁( Element of L) -> Element of the carrier of L = 'not' $1;
consider f being Function of L,L such that
A1: for x being Element of L holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider f = f as Function of L,(L opp) ;
take f ; :: thesis: for x being Element of L holds f . x = 'not' x
thus for x being Element of L holds f . x = 'not' x by A1; :: thesis: verum