let T, T1 be Tree; :: thesis: for P being AntiChain_of_Prefixes of T st P <> {} holds
tree (T,P,T1) = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (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 <> {} implies tree (T,P,T1) = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

assume A1: P <> {} ; :: thesis: tree (T,P,T1) = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

then A2: tree (T,P,T1) = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by Th2;
thus tree (T,P,T1) c= { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } :: according to XBOOLE_0:def 10 :: thesis: { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } c= tree (T,P,T1)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in tree (T,P,T1) or x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

assume x in tree (T,P,T1) ; :: thesis: x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }

then A3: x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by ;
now :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
per cases ( x in P or not x in P ) ;
suppose A4: x in P ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by Th6;
hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) by A4; :: thesis: verum
end;
suppose A5: not x in P ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

now :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
per cases ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
by ;
suppose A6: x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1
}
; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
proof
assume A7: not x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
; :: thesis: contradiction
{ t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \ { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
= P by Th5;
hence contradiction by A5, A6, A7, XBOOLE_0:def 5; :: thesis: verum
end;
hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum
end;
suppose x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum
end;
end;
end;
hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum
end;
end;
end;
hence x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1
}
\/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by XBOOLE_0:def 3; :: thesis: verum
end;
thus { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } c= tree (T,P,T1) by ; :: thesis: verum