let L be non empty LattStr ; :: thesis: ( ( for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v0 "/\" (v0 "\/" v1)) = v0 ) & ( for v0, v1 being Element of L holds (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 ) & ( for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 ) & ( 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 v0, v1 being Element of L st not (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 or ex v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 or 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 A2: for v0, v1 being Element of L holds (v0 "/\" v0) "\/" (v1 "/\" (v0 "\/" v0)) = v0 ; :: thesis: ( ex v1, v0 being Element of L st not (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 or 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 A3: for v1, v0 being Element of L holds (v0 "/\" v1) "\/" (v1 "/\" (v0 "\/" v1)) = v1 ; :: 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
assume not for v0 being Element of L holds v0 "\/" v0 = v0 ; :: thesis: contradiction
then consider C being Element of L such that
A6: C "\/" C <> C ;
A9: for v100 being Element of L holds (v100 "/\" v100) "\/" (v100 "\/" v100) = v100

proof

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

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

end;

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

end;

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;

A17: for v0 being Element of L holds ((v0 "/\" v0) "/\" (v0 "\/" v0)) "\/" ((v0 "/\" v0) "/\" v0) = v0 "/\" v0

proof

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

end;

A20: for v0 being Element of L holds ((v0 "/\" v0) "/\" (v0 "\/" v0)) "\/" ((v0 "\/" v0) "/\" v0) = v0 "\/" v0

proof

let v0 be Element of L; :: thesis: ((v0 "/\" v0) "/\" (v0 "\/" v0)) "\/" ((v0 "\/" v0) "/\" v0) = v0 "\/" v0
(v0 "/\" v0) "\/" (v0 "\/" v0) = v0 by A9;
hence ((v0 "/\" v0) "/\" (v0 "\/" v0)) "\/" ((v0 "\/" v0) "/\" v0) = v0 "\/" v0 by A3; :: thesis: verum

end;

A23: 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;

A26: 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 A23; :: thesis: verum

end;

A29: 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 A26; :: thesis: verum

end;

A31: 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 A29; :: thesis: verum

end;

A33: for v0 being Element of L holds v0 "/\" v0 = v0

proof

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 A31; :: thesis: verum

end;

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

end;

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

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" ((v0 "\/" v0) "/\" v0) = v0 "\/" v0
v0 "/\" v0 = v0 by A33;
hence (v0 "/\" (v0 "\/" v0)) "\/" ((v0 "\/" v0) "/\" v0) = v0 "\/" v0 by A20; :: thesis: verum

end;

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

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" ((v0 "/\" v0) "/\" v0) = v0 "/\" v0
v0 "/\" v0 = v0 by A33;
hence (v0 "/\" (v0 "\/" v0)) "\/" ((v0 "/\" v0) "/\" v0) = v0 "/\" v0 by A17; :: thesis: verum

end;

A39: for v0 being Element of L holds (v0 "/\" (v0 "\/" v0)) "\/" (v0 "/\" v0) = v0 "/\" v0

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" (v0 "/\" v0) = v0 "/\" v0
v0 "/\" v0 = v0 by A33;
hence (v0 "/\" (v0 "\/" v0)) "\/" (v0 "/\" v0) = v0 "/\" v0 by A37; :: thesis: verum

end;

A41: for v0 being Element of L holds (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "/\" v0

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "/\" v0
v0 "/\" v0 = v0 by A33;
hence (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "/\" v0 by A39; :: thesis: verum

end;

A43: for v0 being Element of L holds (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0
v0 "/\" v0 = v0 by A33;
hence (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 by A41; :: thesis: verum

end;

A46: for v102 being Element of L holds (v102 "\/" v102) "/\" v102 = v102

proof

let v102 be Element of L; :: thesis: (v102 "\/" v102) "/\" v102 = v102
(v102 "\/" v102) "/\" (v102 "\/" v102) = v102 "\/" v102 by A33;
hence (v102 "\/" v102) "/\" v102 = v102 by A4; :: thesis: verum

end;

A49: for v0 being Element of L holds (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "\/" v0

proof

let v0 be Element of L; :: thesis: (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "\/" v0
(v0 "\/" v0) "/\" v0 = v0 by A46;
hence (v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 "\/" v0 by A35; :: thesis: verum

end;

for v0 being Element of L holds v0 = v0 "\/" v0

proof

let v0 be Element of L; :: thesis: v0 = v0 "\/" v0
(v0 "/\" (v0 "\/" v0)) "\/" v0 = v0 by A43;
hence v0 = v0 "\/" v0 by A49; :: thesis: verum

end;

hence contradiction by A6; :: thesis: verum