let H be ZF-formula; :: thesis: ( H is atomic implies len H = 3 )
assume A1: H is atomic ; :: thesis: len H = 3

A2: now

assume H is being_equality ; :: thesis: len H = 3
then consider x, y being Variable such that
A3: H = x '=' y by Def10;
H = <*0 ,x,y*> by A3, FINSEQ_1:def 10;
hence len H = 3 by FINSEQ_1:62; :: thesis: verum

end;

now

assume H is being_membership ; :: thesis: len H = 3
then consider x, y being Variable such that
A4: H = x 'in' y by Def11;
H = <*1,x,y*> by A4, FINSEQ_1:def 10;
hence len H = 3 by FINSEQ_1:62; :: thesis: verum

end;

hence len H = 3 by A1, A2, Def15; :: thesis: verum