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 :: thesis: for x being object st x in P holds
x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

let x be object ; :: thesis: ( x in P implies x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
assume A1: 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 11;
then consider q being Element of T such that
A2: q = x by A1;
<*> NAT in T1 by TREES_1:22;
then consider s9 being Element of T1 such that
A3: s9 = <*> NAT ;
q = q ^ s9 by A3, FINSEQ_1:34;
hence x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by A1, A2; :: thesis: verum

end;

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