let A, a, b, c be set ; :: thesis: ( <*a,b,c*> in 3 -tuples_on A implies ( a in A & b in A & c in A ) )
assume <*a,b,c*> in 3 -tuples_on A ; :: thesis: ( a in A & b in A & c in A )
then consider a', b', c' being set such that
A1: ( a' in A & b' in A & c' in A & <*a,b,c*> = <*a',b',c'*> ) by Th12;
( <*a,b,c*> . 1 = a & <*a,b,c*> . 2 = b & <*a,b,c*> . 3 = c & <*a',b',c'*> . 1 = a' & <*a',b',c'*> . 2 = b' & <*a',b',c'*> . 3 = c' ) by FINSEQ_1:62;
hence ( a in A & b in A & c in A ) by A1; :: thesis: verum