deffunc H₁( Element of the adjectives of T) -> Element of the carrier of T = sup ((types $1) \/ (types (non- $1)));
consider f being Function of the adjectives of T, the carrier of T such that
A1: for a being Element of the adjectives of T holds f . a = H₁(a) from FUNCT_2:sch 4();
take f ; :: thesis: for a being adjective of T holds f . a = sup ((types a) \/ (types (non- a)))
thus for a being adjective of T holds f . a = sup ((types a) \/ (types (non- a))) by A1; :: thesis: verum