let A, x be set ; :: thesis: ( x in 2 -tuples_on A iff ex a, b being set st
( a in A & b in A & x = <*a,b*> ) )

hereby :: thesis: ( ex a, b being set st
( a in A & b in A & x = <*a,b*> ) implies x in 2 -tuples_on A )

assume x in 2 -tuples_on A ; :: thesis: ex a, b being set st
( a in A & b in A & x = <*a,b*> )
then x in { s where s is Element of A * : len s = 2 } ;
then consider s being Element of A * such that
A1: x = s and
A2: len s = 2 ;
take a = s . 1; :: thesis: ex b being set st
( a in A & b in A & x = <*a,b*> )
take b = s . 2; :: thesis: ( a in A & b in A & x = <*a,b*> )
A3: ( rng <*a,b*> = {a,b} & a in {a,b} ) by Lm1, TARSKI:def 2;
A4: ( b in {a,b} & rng s c= A ) by RELAT_1:def 19, TARSKI:def 2;
x = <*a,b*> by A1, A2, FINSEQ_1:44;
hence ( a in A & b in A & x = <*a,b*> ) by A1, A3, A4; :: thesis: verum

end;

given a, b being set such that A5: a in A and
A6: b in A and
A7: x = <*a,b*> ; :: thesis: x in 2 -tuples_on A
reconsider A = A as non empty set by A5;
reconsider a = a, b = b as Element of A by A5, A6;
<*a,b*> is Element of 2 -tuples_on A by Th121;
hence x in 2 -tuples_on A by A7; :: thesis: verum