let X be non empty set ; :: thesis: for F, FX being Filter of X st FX = {X} holds
FX is_coarser_than F
let F, FX be Filter of X; :: thesis: ( FX = {X} implies FX is_coarser_than F )
assume A1: FX = {X} ; :: thesis: FX is_coarser_than F
X in F by CARD_FIL:5;
then {X} c= F by TARSKI:def 1;
hence FX is_coarser_than F by A1; :: thesis: verum