let L be non empty upper-bounded Poset; :: thesis: for F being Filter of L holds Top L in F
let F be Filter of L; :: thesis: Top L in F
consider x being Element of F;
Top L >= x by YELLOW_0:45;
hence Top L in F by WAYBEL_0:def 20; :: thesis: verum