let x be set ; :: thesis: for T1, T2 being Tree holds
( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
let T1, T2 be Tree; :: thesis: ( <*x*> in tree (T1,T2) iff ( x = 0 or x = 1 ) )
A1: ( len <*T1,T2*> = 2 & tree (T1,T2) = tree <*T1,T2*> ) by FINSEQ_1:44, TREES_3:def 17;
thus ( not <*x*> in tree (T1,T2) or x = 0 or x = 1 ) :: thesis: ( ( x = 0 or x = 1 ) implies <*x*> in tree (T1,T2) )
proof
assume <*x*> in tree (T1,T2) ; :: thesis: ( x = 0 or x = 1 )
then consider n being Nat, q being FinSequence such that
A2: n < 2 and
q in <*T1,T2*> . (n + 1) and
A3: <*x*> = <*n*> ^ q by A1, TREES_3:def 15;
x = <*x*> . 1 by FINSEQ_1:40
.= n by A3, FINSEQ_1:41 ;
hence ( x = 0 or x = 1 ) by A2, NAT_1:23; :: thesis: verum
end;
assume A4: ( x = 0 or x = 1 ) ; :: thesis: <*x*> in tree (T1,T2)
then reconsider n = x as Element of NAT ;
( <*T1,T2*> . (n + 1) = T1 or <*T1,T2*> . (n + 1) = T2 ) by A4, FINSEQ_1:44;
then A5: {} in <*T1,T2*> . (n + 1) by TREES_1:22;
<*n*> = <*n*> ^ {} by FINSEQ_1:34;
hence <*x*> in tree (T1,T2) by A1, A4, A5, TREES_3:def 15; :: thesis: verum