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; :: thesis: verum

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; :: thesis: verum