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 & <*T1,T2*> . 1 = T1 & <*T1,T2*> . 2 = T2 ) by FINSEQ_1:61;
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 ( x in tree T1,T2 & x <> {} ) ; :: thesis: ex p being FinSequence st
( ( p in T1 & x = <*0 *> ^ p ) or ( p in T2 & x = <*1*> ^ p ) )
then consider n being Element of NAT , q being FinSequence such that
A2: ( n < len <*T1,T2*> & q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q ) by Def15;
1 + 1 = 2 ;
then n <= 1 by A1, A2, NAT_1:13;
then ( n = 1 or n < 0 + 1 ) by XXREAL_0:1;
then ( n = 1 or ( n <= 0 & n >= 0 ) ) by NAT_1:13;
then ( n = 1 or n = 0 ) ;
hence ex p being FinSequence st
( ( p in T1 & x = <*0 *> ^ p ) or ( p in T2 & x = <*1*> ^ p ) ) by A1, A2; :: thesis: verum

end;

now

given q being FinSequence such that A3: ( ( 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
A4: ( ( 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, A4; :: thesis: ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q )
( (<*0 *> ^ q) . 1 = 0 & (<*1*> ^ q) . 1 = 1 & 0 <> 1 ) by FINSEQ_1:58;
hence ( q in <*T1,T2*> . (n + 1) & x = <*n*> ^ q ) by A3, A4, FINSEQ_1:61; :: 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