let B be antichain; :: thesis: for P being FinSequence-membered set holds B ^ P is B -headed
let P be FinSequence-membered set ; :: thesis: B ^ P is B -headed
let p be FinSequence; :: according to POLNOT_1:def 21 :: thesis: ( p in B ^ P implies p is B -headed )
assume p in B ^ P ; :: thesis: p is B -headed
then consider q, r being FinSequence such that
A2: ( p = q ^ r & q in B & r in P ) by Def2;
thus p is B -headed by A2; :: thesis: verum