let a, b, c be odd Prime; :: thesis: ( c - b = 2 & b - a = 2 implies ( a = 3 & b = 5 & c = 7 ) )
assume A1: ( c - b = 2 & b - a = 2 ) ; :: thesis: ( a = 3 & b = 5 & c = 7 )
( 3 divides a or 3 divides b or 3 divides c ) by A1, Th32;
then ( a = 3 or b = 3 or c = 3 ) by INT_2:def 4;
hence ( a = 3 & b = 5 & c = 7 ) by A1, INT_2:def 4; :: thesis: verum