A2: ( H is being_equality or H is being_membership ) by A1, Def15;
A3: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
then consider k being Element of NAT , x, y being Variable such that
A4: H = (<*k*> ^ <*x*>) ^ <*y*> by A2, A3, Def10, Def11;
H = <*k,x,y*> by A4, FINSEQ_1:def 10;
hence H . 2 is Variable by FINSEQ_1:62; :: thesis: verum