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