let r be Sequence of REAL ; :: thesis: for y, s being Sequence
for A, B being Ordinal st B c= A holds
( s,y | A,r | A simplest_on_position B iff s,y,r simplest_on_position B )
let y, s be Sequence; :: thesis: for A, B being Ordinal st B c= A holds
( s,y | A,r | A simplest_on_position B iff s,y,r simplest_on_position B )
let A, B be Ordinal; :: thesis: ( B c= A implies ( s,y | A,r | A simplest_on_position B iff s,y,r simplest_on_position B ) )
assume A1: B c= A ; :: thesis: ( s,y | A,r | A simplest_on_position B iff s,y,r simplest_on_position B )
thus ( s,y | A,r | A simplest_on_position B implies s,y,r simplest_on_position B ) :: thesis: ( s,y,r simplest_on_position B implies s,y | A,r | A simplest_on_position B )

proof

assume A2: s,y | A,r | A simplest_on_position B ; :: thesis: s,y,r simplest_on_position B
let sa be Surreal; :: according to SURREALC:def 15 :: thesis: ( sa = s . B implies ( ( 0 = B implies sa = 0_No ) & ( 0 <> B implies ( sa in_meets_terms s,y,r,B & ( for x being uSurreal st x in_meets_terms s,y,r,B & x <> sa holds
born sa in born x ) ) ) ) )
assume A3: sa = s . B ; :: thesis: ( ( 0 = B implies sa = 0_No ) & ( 0 <> B implies ( sa in_meets_terms s,y,r,B & ( for x being uSurreal st x in_meets_terms s,y,r,B & x <> sa holds
born sa in born x ) ) ) )
thus ( 0 = B implies sa = 0_No ) by A3, A2; :: thesis: ( 0 <> B implies ( sa in_meets_terms s,y,r,B & ( for x being uSurreal st x in_meets_terms s,y,r,B & x <> sa holds
born sa in born x ) ) )
assume A4: B <> 0 ; :: thesis: ( sa in_meets_terms s,y,r,B & ( for x being uSurreal st x in_meets_terms s,y,r,B & x <> sa holds
born sa in born x ) )
sa in_meets_terms s,y | A,r | A,B by A3, A2;
hence sa in_meets_terms s,y,r,B by A1, Th83; :: thesis: for x being uSurreal st x in_meets_terms s,y,r,B & x <> sa holds
born sa in born x
let x be uSurreal; :: thesis: ( x in_meets_terms s,y,r,B & x <> sa implies born sa in born x )
assume A5: ( x in_meets_terms s,y,r,B & x <> sa ) ; :: thesis: born sa in born x
then x in_meets_terms s,y | A,r | A,B by A1, Th83;
hence born sa in born x by A2, A3, A4, A5; :: thesis: verum

end;

assume A6: s,y,r simplest_on_position B ; :: thesis: s,y | A,r | A simplest_on_position B
let sa be Surreal; :: according to SURREALC:def 15 :: thesis: ( sa = s . B implies ( ( 0 = B implies sa = 0_No ) & ( 0 <> B implies ( sa in_meets_terms s,y | A,r | A,B & ( for x being uSurreal st x in_meets_terms s,y | A,r | A,B & x <> sa holds
born sa in born x ) ) ) ) )
assume A7: sa = s . B ; :: thesis: ( ( 0 = B implies sa = 0_No ) & ( 0 <> B implies ( sa in_meets_terms s,y | A,r | A,B & ( for x being uSurreal st x in_meets_terms s,y | A,r | A,B & x <> sa holds
born sa in born x ) ) ) )
thus ( 0 = B implies sa = 0_No ) by A7, A6; :: thesis: ( 0 <> B implies ( sa in_meets_terms s,y | A,r | A,B & ( for x being uSurreal st x in_meets_terms s,y | A,r | A,B & x <> sa holds
born sa in born x ) ) )
assume A8: B <> 0 ; :: thesis: ( sa in_meets_terms s,y | A,r | A,B & ( for x being uSurreal st x in_meets_terms s,y | A,r | A,B & x <> sa holds
born sa in born x ) )
sa in_meets_terms s,y,r,B by A7, A6;
hence sa in_meets_terms s,y | A,r | A,B by A1, Th83; :: thesis: for x being uSurreal st x in_meets_terms s,y | A,r | A,B & x <> sa holds
born sa in born x
let x be uSurreal; :: thesis: ( x in_meets_terms s,y | A,r | A,B & x <> sa implies born sa in born x )
assume A9: ( x in_meets_terms s,y | A,r | A,B & x <> sa ) ; :: thesis: born sa in born x
then x in_meets_terms s,y,r,B by A1, Th83;
hence born sa in born x by A6, A7, A8, A9; :: thesis: verum