set L = QLTLattice1 ;
reconsider z = 0 as Element of QLTLattice1 by ENUMSET1:def 1;
reconsider o = 1 as Element of QLTLattice1 by ENUMSET1:def 1;
reconsider dwa = 2 as Element of QLTLattice1 by ENUMSET1:def 1;
dwa "/\" (dwa "\/" o) = dwa "/\" z by QLTEx1Def
.= z by QLTEx1Def ;
hence not QLTLattice1 is join-absorbing by LATTICES:def 9; :: thesis: verum