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 A2: x in W1 ; :: thesis: x in W2
reconsider p = x as Element of W1 by A2;
A3: p in W2 by A1;
thus x in W2 by A3; :: thesis: verum

end;

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