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
set x = the Element of F;
Top L >= the Element of F by YELLOW_0:45;
hence Top L in F by WAYBEL_0:def 20; :: thesis: verum