let T be Tree; :: thesis: for P being AntiChain_of_Prefixes of T holds P c= { 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
}

let P be AntiChain_of_Prefixes of T; :: thesis: P c= { 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
}

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P 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_proper_prefix_of t1
}
)

assume A1: 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_proper_prefix_of t1
}

ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 ) )
proof
P c= T by TREES_1:def 11;
then consider t9 being Element of T such that
A2: t9 = x by A1;
now :: thesis: for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t9
end;
hence ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 ) ) by A2; :: 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_proper_prefix_of t1
}
; :: thesis: verum