let L be non empty LattStr ; :: thesis: ( L is satisfying_WAL31 & L is satisfying_WAL32 & L is satisfying_WAL33 & L is satisfying_WAL34 & L is satisfying_WAL35 implies ( L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative ) )
assume a1: ( L is satisfying_WAL31 & L is satisfying_WAL32 & L is satisfying_WAL33 & L is satisfying_WAL34 & L is satisfying_WAL35 ) ; :: thesis: ( L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative )
then A2: for v0, v1 being Element of L holds v0 "/\" v1 = v1 "/\" v0 by Lemma3;
for v0, v1 being Element of L holds v0 "\/" v1 = v1 "\/" v0 by a1, Lemma4;
hence ( L is join-idempotent & L is meet-idempotent & L is join-commutative & L is meet-commutative ) by A2, a1, Lemma2, LATTICES:def 4, LATTICES:def 6, Lemma1; :: thesis: verum