consider alpha being Ordinal such that
A1: g in ConwayDay alpha by Def3;
take s = { x where x is Element of ConwayDay alpha : ex f being ConwayGameChain st
( f . 1 = x & f . (len f) = g ) } ; :: thesis: for z being set holds
( z in s iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) )
let z be set ; :: thesis: ( z in s iff ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) )
hereby :: thesis: ( ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) implies z in s )
assume z in s ; :: thesis: ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g )
then consider x being Element of ConwayDay alpha such that
A2: ( x = z & ex f being ConwayGameChain st
( f . 1 = x & f . (len f) = g ) ) ;
thus ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) by A2; :: thesis: verum
end;
assume ex f being ConwayGameChain st
( f . 1 = z & f . (len f) = g ) ; :: thesis: z in s
then consider f being ConwayGameChain such that
A3: ( f . 1 = z & f . (len f) = g ) ;
f . 1 in ConwayDay alpha by Th23, A1, A3;
hence z in s by A3; :: thesis: verum