for L being with_zero GAD_Lattice
for a being Element of L
for X being set st X = { (x "/\" a) where x is Element of L : verum } holds
( X = { x where x is Element of L : x [= a } & X is ClosedSubset of L )