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