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 SUBSET_1:4;
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 Def9;
p "\/" q = p by A1;
then reconsider p9 = p as Element of (latt F) by A2, A3, Th10;
take p9 ; :: according to LATTICES:def 14 :: thesis: for b₁ being Element of the carrier of (latt F) holds
( p9 "\/" b₁ = p9 & b₁ "\/" p9 = p9 )
let r be Element of (latt F); :: thesis: ( p9 "\/" r = p9 & r "\/" p9 = p9 )
reconsider r9 = r as Element of F by A3;
thus p9 "\/" r = p "\/" r9 by Th50
.= p9 by A1 ; :: thesis: r "\/" p9 = p9
hence r "\/" p9 = p9 ; :: thesis: verum