let H be ZF-formula; :: thesis: ( H is atomic implies len H = 3 )
A1: now :: thesis: ( H is being_equality & H is atomic implies len H = 3 )
assume H is being_equality ; :: thesis: ( H is atomic implies len H = 3 )
then consider x, y being Variable such that
A2: H = x '=' y ;
H = <*0,x,y*> by A2, FINSEQ_1:def 10;
hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; :: thesis: verum
end;
A3: now :: thesis: ( H is being_membership & H is atomic implies len H = 3 )
assume H is being_membership ; :: thesis: ( H is atomic implies len H = 3 )
then consider x, y being Variable such that
A4: H = x 'in' y ;
H = <*1,x,y*> by A4, FINSEQ_1:def 10;
hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; :: thesis: verum
end;
assume H is atomic ; :: thesis: len H = 3
hence len H = 3 by A1, A3; :: thesis: verum