let n be Nat; :: thesis: (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3)
(Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (((n + 1) + 1) + 1) by Th11
.= Lucas (n + 3) ;
hence (Lucas (n + 1)) + (Lucas (n + 2)) = Lucas (n + 3) ; :: thesis: verum