defpred S₁[ object ] means ( $1 = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
let T1, T2 be Tree; :: thesis: ( ( for x being object holds
( x in T1 iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) & ( for x being object holds
( x in T2 iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ) ) implies T1 = T2 )
assume that
A48: for x being object holds
( x in T1 iff S₁[x] ) and
A49: for x being object holds
( x in T2 iff S₁[x] ) ; :: thesis: T1 = T2
thus T1 = T2 from XBOOLE_0:sch 2(A48, A49); :: thesis: verum