now :: thesis: for a, b being Element of BL st (UFilter BL) . a = (UFilter BL) . b holds
a = 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;

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 ) )

per cases ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) by A3;

case A4: ( a in UF & not b in UF ) ; :: thesis: (UFilter BL) . a <> (UFilter BL) . b

then UF in (UFilter BL) . a by A2, Th18;
hence (UFilter BL) . a <> (UFilter BL) . b by A4, Th18; :: thesis: verum

end;

case ( not a in UF & b in UF ) ; :: thesis: (UFilter BL) . a <> (UFilter BL) . b

then not UF in (UFilter BL) . a by Th18;
hence (UFilter BL) . a <> (UFilter BL) . b by A2, A3, Th18; :: thesis: verum

end;

end;

end;

hence contradiction by A1; :: thesis: verum

end;

hence UFilter BL is one-to-one by GROUP_6:1; :: thesis: verum