let B, C be antichain; :: thesis: for p being FinSequence st p is B ^ C -headed holds
p is B -headed
let p be FinSequence; :: thesis: ( p is B ^ C -headed implies p is B -headed )
assume p is B ^ C -headed ; :: thesis: p is B -headed
then consider q, r being FinSequence such that
A1: q in B ^ C and
A2: p = q ^ r ;
consider s, t being FinSequence such that
A4: q = s ^ t and
A5: s in B and
t in C by A1, Def2;
p = s ^ (t ^ r) by A2, A4, FINSEQ_1:32;
hence p is B -headed by A5; :: thesis: verum