List of theorems referencing the symbol ULTRAFILTER

(548) Theorem 399: (S /= 0) •imp ((Filter(T,S) & (FORALL x •incin pow(S) | ((x incs T) & Filter(x,S)) •imp (x = T))) •eq Ultrafilter(T,S))
(549) Theorem 400: [Every filter on a set S can be extended to an ultrafilter on S] (Filter(T,S) & (S /= 0)) •imp (EXISTS u | ((u incs T) & Ultrafilter(u,S)))