deffunc H_{1}( 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_{1}(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

consider f being Function of L,L such that

A1: for x being Element of L holds f . x = H

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