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