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