Lucas 2 = Lucas ((0 + 1) + 1)
.= 2 + 1 by Th11
.= 3 ;
hence Lucas 2 = 3 ; :: thesis: verum