let L be Lattice; :: thesis: for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
let F be Filter of L; :: thesis: ( L is upper-bounded implies latt F is upper-bounded )
given p being Element of L such that A1: for q being Element of L holds
( p "\/" q = p & q "\/" p = p ) ; :: according to LATTICES:def 14 :: thesis: latt F is upper-bounded
consider q being Element of L such that
A2: q in F by Th11;
A3: ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def10;
( p "\/" q = p & p "\/" q in F ) by A1, A2, Th10;
then reconsider p' = p as Element of (latt F) by A3;
take p' ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (latt F) holds
( p' "\/" b₁ = p' & b₁ "\/" p' = p' )
let r be Element of (latt F); :: thesis: ( p' "\/" r = p' & r "\/" p' = p' )
reconsider r' = r as Element of F by A3;
thus p' "\/" r = p "\/" r' by Th64
.= p' by A1 ; :: thesis: r "\/" p' = p'
hence r "\/" p' = p' ; :: thesis: verum