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

proof

let v2, v1, v0 be Element of L; :: thesis: v1 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v1
((v0 "/\" v1) "\/" (v2 "/\" v1)) "\/" v1 = v1 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) by A3;
hence v1 "\/" ((v0 "/\" v1) "\/" (v2 "/\" v1)) = v1 by A4; :: thesis: verum

end;

A11: for v100, v102 being Element of L holds v100 "\/" (v102 "/\" v100) = v100

proof

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

end;

for v1, v0 being Element of L holds v0 "\/" (v0 "/\" v1) = v0

proof

let v1, v0 be Element of L; :: thesis: v0 "\/" (v0 "/\" v1) = v0
v1 "/\" v0 = v0 "/\" v1 by A1;
hence v0 "\/" (v0 "/\" v1) = v0 by A11; :: thesis: verum

end;

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