theorem Th25: :: LOPCLSET:25

for BL being non trivial B_Lattice
for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)