theorem TransLat: :: LATTAD_1:25

for L being GAD_Lattice
for x, y, z being Element of L st x [= y & y [= z holds
x [= z