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

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

end;

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