Theorem 1.2 (a \divides b \And b \divides c \c a \divides c) Note 1 (a\divides b) By G Note 2 (b \divides c) By G Note 3 (k_1 \ident \an k \in \nats (b = k \cdot a)) By S Note 4 (k_2 \ident \an k \in \nats (c = k \cdot b)) By S Note 5 (k \ident (k_2 \cdot k_1)) By S Note 6 Line 1 (\true \c \Some k \in \nats (b = k \cdot a) By 1.1;.1 Checked with rules.tex : 135 level: 2 Line 2 \c k_1 \in \nats) By .3 Checked with rules.tex : 3414 level: 68 Note 7 Line 1 (\true \c \Some k \in \nats (c = k \cdot b) By 1.1;.2 Checked with rules.tex : 135 level: 2 Line 2 \c k_2 \in \nats By .4 Checked with rules.tex : 3414 level: 68 Line 3 \c k_2\cdot k_1 \in \nats By 040.44;.6 Checked with rules.tex : 475 level: 2 Line 4 \c k \in \nats) By .5 Checked with rules.tex : 1694 level: 4 Note 8 Line 1 (\true \c \Some k \in \nats (b = k \cdot a) By 1.1;.1 Checked with rules.tex : 135 level: 2 Line 2 \c b = k_1 \cdot a) By .3 Checked with rules.tex : 1843 level: 2 Note 9 Line 1 (\true \c \Some k \in \nats (c = k \cdot b) By 1.1;.2 Checked with rules.tex : 135 level: 2 Line 2 \c c = k_2 \cdot b By .4 Checked with rules.tex : 1843 level: 2 Line 3 \ident k_2 \cdot (k_1 \cdot a) By .8 Checked with rules.tex : 1612 level: 4 Line 4 \ident (k_2 \cdot k_1) \cdot a By 039.7 Checked with rules.tex : 59 level: 0 Line 5 \ident k \cdot a By .5 Checked with rules.tex : 1614 level: 4 Line 6 \c a \divides c) By 1.1; .7 Checked with rules.tex : 3416 level: 2 QED By .9 H .1, .2 Checked with rules.tex : 2161 level: 2 Proof checked.