let z, x, y be set ; :: 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 Th10;
hence ( z `1 = x & z `2 = y ) by TARSKI:def 1; :: thesis: verum