let T1, T2, W1, W2 be Tree; :: thesis: ( T1 c= W1 & T2 c= W2 implies tree (T1,T2) c= tree (W1,W2) )
assume that
A1: T1 c= W1 and
A2: T2 c= W2 ; :: thesis: tree (T1,T2) c= tree (W1,W2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tree (T1,T2) or x in tree (W1,W2) )
assume x in tree (T1,T2) ; :: thesis: x in tree (W1,W2)
then reconsider p = x as Element of tree (T1,T2) ;
( p = {} or ex q being FinSequence st
( ( q in T1 & p = <*0*> ^ q ) or ( q in T2 & p = <*1*> ^ q ) ) ) by Th68;
hence x in tree (W1,W2) by A1, A2, Th68; :: thesis: verum