let A be FinSequenceSet of D; :: thesis: A is FinSequence-membered
let x be object ; :: according to FINSEQ_1:def 18 :: thesis: ( not x in A or x is set )
thus ( not x in A or x is set ) by Def3; :: thesis: verum