let H be ZF-formula; :: thesis: 3 <= len H
now :: thesis: ( not H is atomic implies 3 <= len H )
assume not H is atomic ; :: thesis: 3 <= len H
then consider H1 being ZF-formula such that
A1: (len H1) + 1 <= len H by Th12;
A2: now :: thesis: ( not H1 is atomic implies 3 <= len H )
assume not H1 is atomic ; :: thesis: 3 <= len H
then consider F being ZF-formula such that
A3: (len F) + 1 <= len H1 by Th12;
A4: now :: thesis: ( not F is atomic implies 3 <= len H )
assume not F is atomic ; :: thesis: 3 <= len H
then consider F1 being ZF-formula such that
A5: (len F1) + 1 <= len F by Th12;
0 + 1 <= (len F1) + 1 by XREAL_1:7;
then 1 <= len F by A5, XXREAL_0:2;
then 1 + 1 <= (len F) + 1 by XREAL_1:7;
then 2 <= len H1 by A3, XXREAL_0:2;
then 2 + 1 <= (len H1) + 1 by XREAL_1:7;
hence 3 <= len H by A1, XXREAL_0:2; :: thesis: verum
end;
A6: ((len F) + 1) + 1 <= (len H1) + 1 by A3, XREAL_1:7;
now :: thesis: ( F is atomic implies 3 <= len H )
assume F is atomic ; :: thesis: 3 <= len H
then len F = 3 by Th11;
then (3 + 1) + 1 <= len H by A1, A6, XXREAL_0:2;
hence 3 <= len H by XXREAL_0:2; :: thesis: verum
end;
hence 3 <= len H by A4; :: thesis: verum
end;
now :: thesis: ( H1 is atomic implies 3 <= len H )
assume H1 is atomic ; :: thesis: 3 <= len H
then 3 + 1 <= len H by A1, Th11;
hence 3 <= len H by XXREAL_0:2; :: thesis: verum
end;
hence 3 <= len H by A2; :: thesis: verum
end;
hence 3 <= len H by Th11; :: thesis: verum