set L = QLTLattice1 ;
set f = the L_meet of QLTLattice1;
Y1: for x, y being Element of QLTLattice1 holds x "/\" y = y "/\" x by BINOP_1:def 2;
S1: for x, y, z being Element of QLTLattice1 holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by BINOP_1:def 3;
for x being Element of QLTLattice1 holds x "/\" x = x by BINOP_1:def 4;
hence ( QLTLattice1 is meet-commutative & QLTLattice1 is meet-associative & QLTLattice1 is meet-idempotent ) by Y1, LATTICES:def 6, LATTICES:def 7, S1, SHEFFER1:def 9; :: thesis: verum