let x, y, z be object ; :: thesis: ( z in [:{x},{y}:] implies ( z `1 = x & z `2 = y ) )
assume z in [:{x},{y}:] ; :: thesis: ( z `1 = x & z `2 = y )
then ( z `1 in {x} & z `2 in {y} ) by Th4;
hence ( z `1 = x & z `2 = y ) by TARSKI:def 1; :: thesis: verum