set L = QLTLattice1 ;
let v0, v2, v1 be Element of QLTLattice1; :: according to LATQUASI:def 2 :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)
reconsider z = 0 as Element of QLTLattice1 by ENUMSET1:def 1;

per cases ( ( v0 = v1 & v1 = v2 ) or ( v0 = v1 & v1 <> v2 ) or ( v0 <> v1 & v1 <> v2 ) or ( v0 <> v1 & v1 = v2 ) ) ;

suppose ( v0 = v1 & v1 = v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then ( v1 "/\" v2 = v1 & v0 "\/" v1 = v0 ) by QLTEx1Def;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by SHEFFER1:def 9; :: thesis: verum

end;

suppose ( v0 = v1 & v1 <> v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then A1: ( v1 "/\" v2 = 0 & v0 "\/" v1 = v0 ) by QLTEx1Def;
z "\/" v0 = v0 "\/" z ;
then (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z "/\" v0 by Lemacik00, A1
.= z by Lemacik00
.= v0 "\/" (v1 "/\" v2) by A1, Lemacik001 ;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ; :: thesis: verum

end;

suppose ( v0 <> v1 & v1 <> v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then A1: ( v1 "/\" v2 = 0 & v0 "\/" v1 = 0 ) by QLTEx1Def;
then (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = z by Lemacik00
.= v0 "\/" (v1 "/\" v2) by A1, Lemacik001 ;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) ; :: thesis: verum

end;

suppose ( v0 <> v1 & v1 = v2 ) ; :: thesis: (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2)

then ( v1 "/\" v2 = v1 & v0 "\/" v1 = 0 ) by QLTEx1Def;
hence (v0 "\/" (v1 "/\" v2)) "/\" (v0 "\/" v1) = v0 "\/" (v1 "/\" v2) by Lemacik00; :: thesis: verum

end;

end;