hereby :: thesis: ( ( for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1 ) implies L is satisfying_W3' )

assume A1: L is satisfying_W3' ; :: thesis: for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1
let v2, v1, v0 be Element of L; :: thesis: (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1
((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 by A1;
hence (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1 by LATTICES:def 3; :: thesis: verum

end;

assume for v2, v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v2 "/\" v1) [= v1 ; :: thesis: L is satisfying_W3'
hence L is satisfying_W3' by LATTICES:def 3; :: thesis: verum