let T1, T2 be Tree; :: thesis: for x being set holds
( x in tree (T1,T2) iff ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) )
let x be set ; :: thesis: ( x in tree (T1,T2) iff ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) )
set p = <*T1,T2*>;
A1: len <*T1,T2*> = 2 by FINSEQ_1:44;
A2: <*T1,T2*> . 1 = T1 by FINSEQ_1:44;
A3: <*T1,T2*> . 2 = T2 by FINSEQ_1:44;
thus ( x in tree (T1,T2) & x <> {} implies ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) :: thesis: ( ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) implies x in tree (T1,T2) )

proof

assume that
A4: x in tree (T1,T2) and
A5: x <> {} ; :: thesis: ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) )
consider n being Element of NAT , q being FinSequence such that
A6: n < len <*T1,T2*> and
A7: q in <*T1,T2*> . (n + 1) and
A8: x = <*n*> ^ q by A4, A5, Def15;
1 + 1 = 2 ;
then n <= 1 by A1, A6, NAT_1:13;
then ( n = 1 or n < 0 + 1 ) by XXREAL_0:1;
then ( n = 1 or n = 0 ) by NAT_1:13;
hence ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) by A2, A3, A7, A8; :: thesis: verum

end;

now

given q being FinSequence such that A9: ( ( q in T1 & x = <*0*> ^ q ) or ( q in T2 & x = <*1*> ^ q ) ) ; :: thesis: ex n being Element of NAT ex q being FinSequence st
( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
( x = <*0*> ^ q or x <> <*0*> ^ q ) ;
then consider n being Element of NAT such that
A10: ( ( n = 0 & x = <*0*> ^ q ) or ( n = 1 & x <> <*0*> ^ q ) ) ;
take n = n; :: thesis: ex q being FinSequence st
( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
take q = q; :: thesis: ( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
thus n < len <*T1,T2*> by A1, A10; :: thesis: ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
(<*0*> ^ q) . 1 = 0 by FINSEQ_1:41;
hence ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q ) by A9, A10, FINSEQ_1:41, FINSEQ_1:44; :: thesis: verum

end;

hence ( ( x = {} or ex p being FinSequence st
( ( p in T1 & x = <*0*> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) ) implies x in tree (T1,T2) ) by Def15; :: thesis: verum