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 }

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 }

hence
P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
; :: thesis: verumx 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;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