:: deftheorem defines satisfying_WAL4 LATWAL_1:def 16 :
for L being non empty LattStr holds
( L is satisfying_WAL4 iff for v2, v0, v5, v4, v3, v1 being Element of L holds (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "/\" v2) "\/" (((v0 "/\" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)) "\/" (((v1 "/\" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)) "\/" (v5 "/\" (v1 "\/" (((v1 "\/" v3) "/\" (v4 "\/" v1)) "/\" v1)))) "/\" (v0 "\/" (((v1 "/\" v3) "\/" (v4 "/\" v1)) "\/" v1)))) "/\" (((v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1))) "\/" v2)) = v1 );