let L be Lattice; :: thesis: for p being Element of L st {p} is Filter of L holds
L is upper-bounded
let p be Element of L; :: thesis: ( {p} is Filter of L implies L is upper-bounded )
assume {p} is Filter of L ; :: thesis: L is upper-bounded
then reconsider F = {p} as Filter of L ;
take p ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of L holds
( p "\/" b₁ = p & b₁ "\/" p = p )
let q be Element of L; :: thesis: ( p "\/" q = p & q "\/" p = p )
p in F by TARSKI:def 1;
then p "\/" q in F by Th10;
hence ( p "\/" q = p & q "\/" p = p ) by TARSKI:def 1; :: thesis: verum