let L be GAD_Lattice; :: thesis: for x being Element of L holds x [= x
let x be Element of L; :: thesis: x [= x
x "/\" x = x by IMeet;
hence x [= x by LATTICES:4; :: thesis: verum