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 join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent ) by Y1, LATTICES:def 4, LATTICES:def 5, S1, ROBBINS1:def 7; :: 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 join-commutative & QLTLattice2 is join-associative & QLTLattice2 is join-idempotent ) by Y1, LATTICES:def 4, LATTICES:def 5, S1, ROBBINS1:def 7; :: thesis: verum