now :: thesis: for a, b being Element of BL st (UFilter BL) . a = (UFilter BL) . b holds

a = b

hence
UFilter BL is one-to-one
by GROUP_6:1; :: thesis: veruma = b

let a, b be Element of BL; :: thesis: ( (UFilter BL) . a = (UFilter BL) . b implies a = b )

assume A1: (UFilter BL) . a = (UFilter BL) . b ; :: thesis: a = b

assume not a = b ; :: thesis: contradiction

then consider UF being Filter of BL such that

A2: UF is being_ultrafilter and

A3: ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) by FILTER_0:47;

end;assume A1: (UFilter BL) . a = (UFilter BL) . b ; :: thesis: a = b

assume not a = b ; :: thesis: contradiction

then consider UF being Filter of BL such that

A2: UF is being_ultrafilter and

A3: ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) by FILTER_0:47;

now :: thesis: ( ( a in UF & not b in UF & (UFilter BL) . a <> (UFilter BL) . b ) or ( not a in UF & b in UF & (UFilter BL) . a <> (UFilter BL) . b ) )

hence
contradiction
by A1; :: thesis: verumend;