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