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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ B or x in C ^^ D )
assume x in A ^^ B ; :: thesis: x in C ^^ D
then consider a, b being Element of E ^omega such that
A2: ( a in A & b in B & x = a ^ b ) by Def1;
thus x in C ^^ D by A1, A2, Def1; :: thesis: verum

end;