Lucas 3 = Lucas ((1 + 1) + 1)
.= 3 + 1 by Th11, Th14
.= 4 ;
hence Lucas 3 = 4 ; :: thesis: verum