let BL be non trivial B_Lattice; :: thesis: UFilter BL is one-to-one

now

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 & ( ( a in UF & not b in UF ) or ( not a in UF & b in UF ) ) ) by FILTER_0:60;

now

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

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

then UF in (UFilter BL) . a by A2, Th21;
hence (UFilter BL) . a <> (UFilter BL) . b by A3, Th21; :: 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 Th21;
hence (UFilter BL) . a <> (UFilter BL) . b by A2, Th21; :: 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