let T, T1 be Tree; :: thesis: for P being AntiChain_of_Prefixes of T holds P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
let P be AntiChain_of_Prefixes of T; :: thesis: P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

now

let x be set ; :: thesis: ( x in P implies x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
assume A2: x in P ; :: thesis: x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
P c= T by TREES_1:def 14;
then consider q being Element of T such that
A4: q = x by A2;
<*> NAT in T1 by TREES_1:47;
then consider s9 being Element of T1 such that
A6: s9 = <*> NAT ;
q = q ^ s9 by A6, FINSEQ_1:47;
hence x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by A2, A4; :: thesis: verum

end;

hence P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by TARSKI:def 3; :: thesis: verum