let P, Q, R be FinSequence-membered set ; :: thesis: ( P c= R * & Q c= R * implies P ^ Q c= R * )
assume that
A1: P c= R * and
A2: Q c= R * ; :: thesis: P ^ Q c= R *
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P ^ Q or a in R * )
assume a in P ^ Q ; :: thesis: a in R *
then consider p, q being FinSequence such that
A3: a = p ^ q and
A4: p in P and
A5: q in Q by Def2;
thus a in R * by A1, A2, A3, A4, A5, Th12; :: thesis: verum