A1: 2 -' 1 = 2 - 1 by XREAL_1:235
.= 1 ;
4 -' 2 = 4 - 2 by XREAL_1:235
.= 2 ;
then Catalan 2 = 2 / 2 by A1, NEWTON:33
.= 1 ;
hence Catalan 2 = 1 ; :: thesis: verum