let x be set ; :: thesis: ( x is triple implies x is pair )
assume ex x1, x2, x3 being set st x = [x1,x2,x3] ; :: according to XTUPLE_0:def 5 :: thesis: x is pair
hence x is pair ; :: thesis: verum