let L be Nelson_Algebra; :: thesis: ( L is satisfying_N1* & L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N1* by Th24; :: thesis: ( L is satisfying_N2* & L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N2* by Th25; :: thesis: ( L is satisfying_N3* & L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N3* by Th23; :: thesis: ( L is satisfying_N4* & L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N4* ; :: thesis: ( L is satisfying_N5* & L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N5* :: thesis: ( L is satisfying_N6* & L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )

proof

now :: thesis: for a, b being Element of L holds (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a)

let a, b be Element of L; :: thesis: (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a)
set ab = a =-> b;
set ba = b =-> a;
A1: (a =-> b) => ((b =-> a) => b) < (b =-> a) => ((a =-> b) => a)

proof

A2: b < (b => a) => a by Th19;
A3: (b => a) => a < ((- a) => (- b)) => ((b => a) => a) by Th24;
A4: ((- a) => (- b)) => ((b => a) => a) = (((- a) => (- b)) "/\" (b => a)) => a by Lm3;
b < (b =-> a) => a by Def3, A2, A3, A4;
then (b =-> a) => b < (b =-> a) => ((b =-> a) => a) by Th38;
then (a =-> b) => ((b =-> a) => b) < (a =-> b) => ((b =-> a) => ((b =-> a) => a)) by Th38;
then (a =-> b) => ((b =-> a) => b) < (a =-> b) => (((b =-> a) "/\" (b =-> a)) => a) by Lm3;
hence (a =-> b) => ((b =-> a) => b) < (b =-> a) => ((a =-> b) => a) by Th18; :: thesis: verum

end;

A5: (- a) "/\" ((- a) => (- b)) < - b by Th17;
A6: - ((b =-> a) => ((a =-> b) => a)) < - ((a =-> b) => ((b =-> a) => b))

proof

A7: (a =-> b) "/\" (b =-> a) < (a =-> b) "/\" (b =-> a) by Def2;
((a =-> b) "/\" (b =-> a)) "/\" ((- a) "/\" ((- a) => (- b))) = (((a =-> b) "/\" (b => a)) "/\" ((- a) => (- b))) "/\" ((- a) "/\" ((- a) => (- b))) by LATTICES:def 7
.= ((((a =-> b) "/\" (b => a)) "/\" ((- a) => (- b))) "/\" ((- a) => (- b))) "/\" (- a) by LATTICES:def 7
.= (((a =-> b) "/\" (b => a)) "/\" (((- a) => (- b)) "/\" ((- a) => (- b)))) "/\" (- a) by LATTICES:def 7
.= ((a =-> b) "/\" ((b => a) "/\" ((- a) => (- b)))) "/\" (- a) by LATTICES:def 7
.= (a =-> b) "/\" ((b =-> a) "/\" (- a)) by LATTICES:def 7 ;
then A8: (a =-> b) "/\" ((b =-> a) "/\" (- a)) < ((a =-> b) "/\" (b =-> a)) "/\" (- b) by A7, Lm2, A5;
- ((b =-> a) => a) < (b =-> a) "/\" (- a) by Def10;
then A9: (a =-> b) "/\" (- ((b =-> a) => a)) < (a =-> b) "/\" ((b =-> a) "/\" (- a)) by Lm1;
A10: - ((a =-> b) => ((b =-> a) => a)) < (a =-> b) "/\" (- ((b =-> a) => a)) by Def10;
(b =-> a) "/\" (- b) < - ((b =-> a) => b) by Def9;
then A11: (a =-> b) "/\" ((b =-> a) "/\" (- b)) < (a =-> b) "/\" (- ((b =-> a) => b)) by Lm1;
(a =-> b) "/\" (- ((b =-> a) => b)) < - ((a =-> b) => ((b =-> a) => b)) by Def9;
then (a =-> b) "/\" ((b =-> a) "/\" (- b)) < - ((a =-> b) => ((b =-> a) => b)) by Def3, A11;
then ((a =-> b) "/\" (b =-> a)) "/\" (- b) < - ((a =-> b) => ((b =-> a) => b)) by LATTICES:def 7;
then (a =-> b) "/\" ((b =-> a) "/\" (- a)) < - ((a =-> b) => ((b =-> a) => b)) by Def3, A8;
then (a =-> b) "/\" (- ((b =-> a) => a)) < - ((a =-> b) => ((b =-> a) => b)) by Def3, A9;
then - ((a =-> b) => ((b =-> a) => a)) < - ((a =-> b) => ((b =-> a) => b)) by Def3, A10;
hence - ((b =-> a) => ((a =-> b) => a)) < - ((a =-> b) => ((b =-> a) => b)) by Th18; :: thesis: verum

end;

A12: (b =-> a) => ((a =-> b) => a) < (a =-> b) => ((b =-> a) => b)

proof

A13: a < (a => b) => b by Th19;
A14: (a => b) => b < ((- b) => (- a)) => ((a => b) => b) by Th24;
A15: ((- b) => (- a)) => ((a => b) => b) = (((- b) => (- a)) "/\" (a => b)) => b by Lm3;
a < (a =-> b) => b by Def3, A13, A14, A15;
then (a =-> b) => a < (a =-> b) => ((a =-> b) => b) by Th38;
then (b =-> a) => ((a =-> b) => a) < (b =-> a) => ((a =-> b) => ((a =-> b) => b)) by Th38;
then (b =-> a) => ((a =-> b) => a) < (b =-> a) => (((a =-> b) "/\" (a =-> b)) => b) by Lm3;
hence (b =-> a) => ((a =-> b) => a) < (a =-> b) => ((b =-> a) => b) by Th18; :: thesis: verum

end;

A16: - ((a =-> b) => ((b =-> a) => b)) < - ((b =-> a) => ((a =-> b) => a))

proof

A17: (- b) "/\" ((- b) => (- a)) < - a by Th17;
A18: (b =-> a) "/\" (a =-> b) < (b =-> a) "/\" (a =-> b) by Def2;
((b =-> a) "/\" (a =-> b)) "/\" ((- b) "/\" ((- b) => (- a))) = (((b =-> a) "/\" (a => b)) "/\" ((- b) => (- a))) "/\" ((- b) "/\" ((- b) => (- a))) by LATTICES:def 7
.= ((((b =-> a) "/\" (a => b)) "/\" ((- b) => (- a))) "/\" ((- b) => (- a))) "/\" (- b) by LATTICES:def 7
.= (((b =-> a) "/\" (a => b)) "/\" (((- b) => (- a)) "/\" ((- b) => (- a)))) "/\" (- b) by LATTICES:def 7
.= ((b =-> a) "/\" ((a => b) "/\" ((- b) => (- a)))) "/\" (- b) by LATTICES:def 7
.= (b =-> a) "/\" ((a =-> b) "/\" (- b)) by LATTICES:def 7 ;
then A19: (b =-> a) "/\" ((a =-> b) "/\" (- b)) < ((b =-> a) "/\" (a =-> b)) "/\" (- a) by A18, Lm2, A17;
- ((a =-> b) => b) < (a =-> b) "/\" (- b) by Def10;
then A20: (b =-> a) "/\" (- ((a =-> b) => b)) < (b =-> a) "/\" ((a =-> b) "/\" (- b)) by Lm1;
A21: - ((b =-> a) => ((a =-> b) => b)) < (b =-> a) "/\" (- ((a =-> b) => b)) by Def10;
(a =-> b) "/\" (- a) < - ((a =-> b) => a) by Def9;
then A22: (b =-> a) "/\" ((a =-> b) "/\" (- a)) < (b =-> a) "/\" (- ((a =-> b) => a)) by Lm1;
(b =-> a) "/\" (- ((a =-> b) => a)) < - ((b =-> a) => ((a =-> b) => a)) by Def9;
then (b =-> a) "/\" ((a =-> b) "/\" (- a)) < - ((b =-> a) => ((a =-> b) => a)) by Def3, A22;
then ((b =-> a) "/\" (a =-> b)) "/\" (- a) < - ((b =-> a) => ((a =-> b) => a)) by LATTICES:def 7;
then (b =-> a) "/\" ((a =-> b) "/\" (- b)) < - ((b =-> a) => ((a =-> b) => a)) by Def3, A19;
then (b =-> a) "/\" (- ((a =-> b) => b)) < - ((b =-> a) => ((a =-> b) => a)) by Def3, A20;
then - ((b =-> a) => ((a =-> b) => b)) < - ((b =-> a) => ((a =-> b) => a)) by Def3, A21;
hence - ((a =-> b) => ((b =-> a) => b)) < - ((b =-> a) => ((a =-> b) => a)) by Th18; :: thesis: verum

end;

A23: (a =-> b) => ((b =-> a) => b) <= (b =-> a) => ((a =-> b) => a) by A6, A1, Th5;
(b =-> a) => ((a =-> b) => a) <= (a =-> b) => ((b =-> a) => b) by A12, A16, Th5;
hence (a =-> b) => ((b =-> a) => b) = (b =-> a) => ((a =-> b) => a) by A23, Th3; :: thesis: verum

end;

hence L is satisfying_N5* ; :: thesis: verum

end;

thus L is satisfying_N6* by Th26; :: thesis: ( L is satisfying_N7* & L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N7* by Th27; :: thesis: ( L is satisfying_N8* & L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N8* by Th28; :: thesis: ( L is satisfying_N9* & L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N9* by Th29; :: thesis: ( L is satisfying_N10* & L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N10* by Th30; :: thesis: ( L is satisfying_N11* & L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N11* by Th31; :: thesis: ( L is satisfying_N12* & L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N12* by Th32; :: thesis: ( L is satisfying_N13* & L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N13* by Th33; :: thesis: ( L is satisfying_N14* & L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N14* by Th34; :: thesis: ( L is satisfying_N15* & L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N15* by Th35; :: thesis: ( L is satisfying_N16* & L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N16* ; :: thesis: ( L is satisfying_N17* & L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N17* by Th37; :: thesis: ( L is satisfying_N18* & L is satisfying_N19* )
thus L is satisfying_N18* ; :: thesis: L is satisfying_N19*
thus L is satisfying_N19* by Th36; :: thesis: verum