let B be antichain; :: thesis: for p, q, r, s being FinSequence st p ^ q = r ^ s & p in B & r in B holds
( p = r & q = s )
let p, q, r, s be FinSequence; :: thesis: ( p ^ q = r ^ s & p in B & r in B implies ( p = r & q = s ) )
assume that
A2: p ^ q = r ^ s and
A3: ( p in B & r in B ) ; :: thesis: ( p = r & q = s )
consider t being FinSequence such that
A4: ( p ^ t = r or p = r ^ t ) by Th1, A2;
thus p = r by A3, A4, Th40; :: thesis: q = s
hence q = s by A2, FINSEQ_1:33; :: thesis: verum