let E be set ; :: thesis: for A, C, B being Subset of (E ^omega ) st A c= C + & B c= C + holds
A ^^ B c= C +
let A, C, B be Subset of (E ^omega ); :: thesis: ( A c= C + & B c= C + implies A ^^ B c= C + )
assume A1: ( A c= C + & B c= C + ) ; :: thesis: A ^^ B c= C +

now

let x be set ; :: thesis: ( x in A ^^ B implies x in C + )
assume x in A ^^ B ; :: thesis: x in C +
then consider a, b being Element of E ^omega such that
A2: ( a in A & b in B & x = a ^ b ) by FLANG_1:def 1;
thus x in C + by A1, A2, Th66; :: thesis: verum

end;

hence A ^^ B c= C + by TARSKI:def 3; :: thesis: verum