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 set ; :: 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 Th71;
hence x in tree W1,W2 by A1, A2, Th71; :: thesis: verum