thus card (((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1))) ';' (SubFrom (GBP,3,GBP,2))) = (card ((if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1))))) ';' ((GBP,3) := (GBP,1)))) + 1 by SCMP_GCD:4
.= ((card (if>0 (GBP,3,(Load (SubFrom (GBP,1,GBP,2))),(Load (SubFrom (GBP,2,GBP,1)))))) + 1) + 1 by SCMP_GCD:4
.= ((((card (Load (SubFrom (GBP,1,GBP,2)))) + (card (Load (SubFrom (GBP,2,GBP,1))))) + 2) + 1) + 1 by SCMPDS_6:65
.= (((1 + (card (Load (SubFrom (GBP,2,GBP,1))))) + 2) + 1) + 1 by COMPOS_1:54
.= (((1 + 1) + 2) + 1) + 1 by COMPOS_1:54
.= 6 ; :: thesis: verum