set L = QLTLattice2 ;

Y1: for x, y being Element of QLTLattice2 holds x "/\" y = y "/\" x by BINOP_1:def 2;

S1: for x, y, z being Element of QLTLattice2 holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by BINOP_1:def 3;

for x being Element of QLTLattice2 holds x "/\" x = x by BINOP_1:def 4;

hence ( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent ) by Y1, LATTICES:def 6, LATTICES:def 7, S1, SHEFFER1:def 9; :: thesis: verum

Y1: for x, y being Element of QLTLattice2 holds x "/\" y = y "/\" x by BINOP_1:def 2;

S1: for x, y, z being Element of QLTLattice2 holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by BINOP_1:def 3;

for x being Element of QLTLattice2 holds x "/\" x = x by BINOP_1:def 4;

hence ( QLTLattice2 is meet-commutative & QLTLattice2 is meet-associative & QLTLattice2 is meet-idempotent ) by Y1, LATTICES:def 6, LATTICES:def 7, S1, SHEFFER1:def 9; :: thesis: verum