theorem Th21: :: LOPCLSET:21

for BL being non trivial B_Lattice
for a, b being Element of BL holds (UFilter BL) . (a "\/" b) = ((UFilter BL) . a) \/ ((UFilter BL) . b)