set L = QLTLattice1 ;

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

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