let A be FinSequence-membered set ; :: thesis: A ^^ {} c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ {} or x in A )
assume x in A ^^ {} ; :: thesis: x in A
then ex p being Element of A ex q being Element of {} st
( x = p ^ q & p in A & q in {} ) ;
hence x in A ; :: thesis: verum