deffunc H₁( object ) -> set = { F where F is Filter of BL : ( F is being_ultrafilter & $1 in F ) } ;
consider f being Function such that
A1: dom f = the carrier of BL and
A2: for x being object st x in the carrier of BL holds
f . x = H₁(x) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) )
thus ( dom f = the carrier of BL & ( for a being Element of BL holds f . a = { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ) ) by A1, A2; :: thesis: verum