theorem :: LATTAD_1:71

for L being with_zero GAD_Lattice
for a being Element of L
for S being non empty ClosedSubset of L
for b being Element of (latt (L,S)) st b = a & S = { (x "/\" a) where x is Element of L : verum } holds
( latt (L,S) is Lattice-like & latt (L,S) is distributive & ( for c being Element of (latt (L,S)) holds
( b "\/" c = b & c "\/" b = b & c [= b ) ) )