let L be GAD_Lattice; :: thesis: for x, y, z being Element of L st x [= y & y [= z holds
x [= z
let x, y, z be Element of L; :: thesis: ( x [= y & y [= z implies x [= z )
assume A0: ( x [= y & y [= z ) ; :: thesis: x [= z
then ( x "/\" y = x & y "/\" z = y ) by LATTICES:4;
then A1: x "/\" (y "/\" z) = x "/\" z by LATTICES:def 7;
x "/\" (y "/\" z) = x "/\" y by LATTICES:def 9, A0
.= x by A0, LATTICES:4 ;
hence x [= z by LATTICES:4, A1; :: thesis: verum