let L be non empty LattStr ; :: thesis: ( ( for v0 being Element of L holds v0 "\/" v0 = v0 ) & ( for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ) implies for v1, v2 being Element of L holds v1 "/\" (v1 "\/" v2) = v1 )
assume A1: for v0 being Element of L holds v0 "\/" v0 = v0 ; :: thesis: ( ex v1, v2, v0 being Element of L st not v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 or for v1, v2 being Element of L holds v1 "/\" (v1 "\/" v2) = v1 )
assume A2: for v1, v2, v0 being Element of L holds v0 "/\" (v1 "\/" (v0 "\/" v2)) = v0 ; :: thesis: for v1, v2 being Element of L holds v1 "/\" (v1 "\/" v2) = v1
for v102, v100 being Element of L holds v100 "/\" (v100 "\/" v102) = v100

proof

let v102, v100 be Element of L; :: thesis: v100 "/\" (v100 "\/" v102) = v100
(v100 "\/" v102) "\/" (v100 "\/" v102) = v100 "\/" v102 by A1;
hence v100 "/\" (v100 "\/" v102) = v100 by A2; :: thesis: verum

end;

hence for v1, v2 being Element of L holds v1 "/\" (v1 "\/" v2) = v1 ; :: thesis: verum