let W1, W2 be Tree; :: thesis: ( ( for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) ) implies W1 = W2 )
assume A1: for p being FinSequence of NAT holds
( p in W1 iff p in W2 ) ; :: thesis: W1 = W2
thus W1 c= W2 :: according to XBOOLE_0:def 10 :: thesis: W2 c= W1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W1 or x in W2 )
assume x in W1 ; :: thesis: x in W2
then reconsider p = x as Element of W1 ;
p in W2 by A1;
hence x in W2 ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W2 or x in W1 )
assume x in W2 ; :: thesis: x in W1
then reconsider p = x as Element of W2 ;
p in W1 by A1;
hence x in W1 ; :: thesis: verum