let Z1, Z2 be Tree; :: thesis: for p being FinSequence of NAT st p in Z1 holds
for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
let p be FinSequence of NAT ; :: thesis: ( p in Z1 implies for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w )
assume A1: p in Z1 ; :: thesis: for v being Element of Z1 with-replacement p,Z2
for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
set Z = Z1 with-replacement p,Z2;
let v be Element of Z1 with-replacement p,Z2; :: thesis: for w being Element of Z1 st v = w & not p,w are_c=-comparable holds
succ v = succ w
let w be Element of Z1; :: thesis: ( v = w & not p,w are_c=-comparable implies succ v = succ w )
assume A2: ( v = w & not p,w are_c=-comparable ) ; :: thesis: succ v = succ w
then A3: ( not w is_a_prefix_of p & not p is_a_prefix_of w ) by XBOOLE_0:def 9;

now

let x be set ; :: thesis: ( ( x in succ v implies x in succ w ) & ( x in succ w implies x in succ v ) )
thus ( x in succ v implies x in succ w ) :: thesis: ( x in succ w implies x in succ v )

proof

assume x in succ v ; :: thesis: x in succ w
then x in { (v ^ <*n*>) where n is Element of NAT : v ^ <*n*> in Z1 with-replacement p,Z2 } by TREES_2:def 5;
then consider n being Element of NAT such that
A4: ( x = v ^ <*n*> & v ^ <*n*> in Z1 with-replacement p,Z2 ) ;
reconsider x' = x as FinSequence of NAT by A4;
v ^ <*n*> in Z1

proof

assume A5: not v ^ <*n*> in Z1 ; :: thesis: contradiction
then ex t being FinSequence of NAT st
( t in Z2 & x' = p ^ t ) by A1, A4, TREES_1:def 12;
then A6: p is_a_prefix_of v ^ <*n*> by A4, TREES_1:8;

per cases ( p is_a_proper_prefix_of v ^ <*n*> or p = v ^ <*n*> ) by A6, XBOOLE_0:def 8;

suppose p is_a_proper_prefix_of v ^ <*n*> ; :: thesis: contradiction

hence contradiction by A2, A3, TREES_1:32; :: thesis: verum

end;

suppose p = v ^ <*n*> ; :: thesis: contradiction

hence contradiction by A1, A5; :: thesis: verum

end;

end;

end;

then x in { (w ^ <*m*>) where m is Element of NAT : w ^ <*m*> in Z1 } by A2, A4;
hence x in succ w by TREES_2:def 5; :: thesis: verum

end;

assume x in succ w ; :: thesis: x in succ v
then x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in Z1 } by TREES_2:def 5;
then consider n being Element of NAT such that
A7: ( x = w ^ <*n*> & w ^ <*n*> in Z1 ) ;
not p is_a_proper_prefix_of w ^ <*n*> by A3, TREES_1:32;
then v ^ <*n*> in Z1 with-replacement p,Z2 by A1, A2, A7, TREES_1:def 12;
then x in { (v ^ <*m*>) where m is Element of NAT : v ^ <*m*> in Z1 with-replacement p,Z2 } by A2, A7;
hence x in succ v by TREES_2:def 5; :: thesis: verum

end;

hence succ v = succ w by TARSKI:2; :: thesis: verum