let t1, t2 be set ; :: thesis: ( ( for z being set holds
( z in t1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) & ( for z being set holds
( z in t2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ) implies t1 = t2 )
assume A4: for z being set holds
( z in t1 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ; :: thesis: ( ex z being set st
( ( z in t2 implies ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) implies ( ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) & not z in t2 ) ) or t1 = t2 )
assume A5: for z being set holds
( z in t2 iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ) ; :: thesis: t1 = t2

now :: thesis: for z being object holds
( ( z in t1 implies z in t2 ) & ( z in t2 implies z in t1 ) )

let z be object ; :: thesis: ( ( z in t1 implies z in t2 ) & ( z in t2 implies z in t1 ) )

hereby :: thesis: ( z in t2 implies z in t1 )

assume z in t1 ; :: thesis: z in t2
then ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A4;
hence z in t2 by A5; :: thesis: verum

end;

hereby :: thesis: verum

assume z in t2 ; :: thesis: z in t1
then ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A5;
hence z in t1 by A4; :: thesis: verum

end;

end;

hence t1 = t2 by TARSKI:2; :: thesis: verum