let S be Subset of L; :: thesis: ( S is final implies S is join-closed )
assume Z: S is final ; :: thesis: S is join-closed
let p, q be Element of L; :: according to LATTICES:def 25 :: thesis: ( p in S & q in S implies p "\/" q in S )
assume that
p in S and
Z2: q in S ; :: thesis: p "\/" q in S
q [= p "\/" q by Th22;
hence p "\/" q in S by Z, Z2, Defy; :: thesis: verum