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