theorem :: LATWAL_1:7

for L being WA_Lattice
for x being Element of L holds x [= x ;