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