let H be ZF-formula; :: thesis: ( len H = 3 implies H is atomic )
assume A1: len H = 3 ; :: thesis: H is atomic
assume not H is atomic ; :: thesis: contradiction
then consider H1 being ZF-formula such that
A2: (len H1) + 1 <= len H by Th12;
3 <= len H1 by Th13;
then 3 + 1 <= (len H1) + 1 by XREAL_1:7;
hence contradiction by A1, A2, XXREAL_0:2; :: thesis: verum