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

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

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

end;

given a, b, c being set such that A6: a in A and
A7: ( b in A & c in A ) and
A8: x = <*a,b,c*> ; :: thesis: x in 3 -tuples_on A
reconsider A = A as non empty set by A6;
reconsider a = a, b = b, c = c as Element of A by A6, A7;
<*a,b,c*> is Element of 3 -tuples_on A by Th124;
hence x in 3 -tuples_on A by A8; :: thesis: verum