theorem Th391i4: :: LATTAD_1:45

for L being GAD_Lattice
for x, y being Element of L holds
( x "/\" y = y "/\" x iff y "/\" x [= y ) by LATTICES:def 8, Th3715;