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

proof

now :: thesis: for v101, v2, v1, v100 being Element of L holds ((v100 "\/" v101) "/\" v100) "/\" v100 = v100

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

end;

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

end;

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

proof

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

end;

A32: for v2, v1, v101 being Element of L holds (((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101) "/\" (((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101) = ((v101 "\/" v1) "/\" (v2 "\/" v101)) "/\" v101

proof

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

end;

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

proof

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

end;

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

proof

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

end;

now :: thesis: for v2, v1, v0 being Element of L holds v0 "/\" v0 = v0

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

end;

hence for v0 being Element of L holds v0 "/\" v0 = v0 ; :: thesis: verum