let S be Subset of L; :: thesis: ( S is initial implies S is meet-closed )
assume A2: S is initial ; :: thesis: S is meet-closed
let p, q be Element of L; :: according to LATTICES:def 24 :: thesis: ( p in S & q in S implies p "/\" q in S )
assume that
p in S and
A3: q in S ; :: thesis: p "/\" q in S
p "/\" q [= q by Th23;
hence p "/\" q in S by A2, A3, Def22; :: thesis: verum