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