let g be ConwayGame; :: thesis: for s being set st g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) holds
the_Tree_of g c= s
let s be set ; :: thesis: ( g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) implies the_Tree_of g c= s )
assume A1: ( g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) ) ; :: thesis: the_Tree_of g c= s
hereby :: according to TARSKI:def 3 :: thesis: verum
let z be object ; :: thesis: ( z in the_Tree_of g implies z in s )
assume z in the_Tree_of g ; :: thesis: z in s
then consider f being ConwayGameChain such that
A2: ( f . 1 = z & f . (len f) = g ) by Def12;
defpred S2[ Nat] means ( $1 + 1 <= len f & f . ($1 + 1) in s );
len f > 0 ;
then reconsider m = (len f) - 1 as Nat by NAT_1:20;
S2[m] by A2, A1;
then A3: ex k being Nat st S2[k] ;
A4: for k being Nat st k <> 0 & S2[k] holds
ex n being Nat st
( n < k & S2[n] )
proof
let k be Nat; :: thesis: ( k <> 0 & S2[k] implies ex n being Nat st
( n < k & S2[n] ) )
assume A5: ( k <> 0 & S2[k] ) ; :: thesis: ex n being Nat st
( n < k & S2[n] )
then reconsider m = k - 1 as Nat by NAT_1:20;
take m ; :: thesis: ( m < k & S2[m] )
thus m < k by XREAL_1:147; :: thesis: S2[m]
then m + 1 < k + 1 by XREAL_1:6;
hence m + 1 <= len f by A5, XXREAL_0:2; :: thesis: f . (m + 1) in s
A6: k + 1 > 1 by A5, XREAL_1:29;
then reconsider k1 = k + 1 as Element of dom f by A5, FINSEQ_3:25;
( f . (k1 - 1) in the_Options_of (f . k1) & the_Options_of (f . k1) c= s ) by Def11, A1, A5, A6;
hence f . (m + 1) in s ; :: thesis: verum
end;
S2[ 0 ] from NAT_1:sch 7(A3, A4);
hence z in s by A2; :: thesis: verum
end;