let S be Subset of L; :: thesis: ( S is final implies S is join-closed )
assume A4: 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
A5: q in S ; :: thesis: p "\/" q in S
q [= p "\/" q by Th22;
hence p "\/" q in S by A4, A5, Def23; :: thesis: verum