let E be set ; :: thesis: for A, B, C being Subset of (E ^omega) st A c= C * & B c= C * holds
A ^^ B c= C *
let A, B, C 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 *
thus A ^^ B c= C * :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ B or x in C * )
assume x in A ^^ B ; :: thesis: x in C *
then ex a, b being Element of E ^omega st
( a in A & b in B & x = a ^ b ) by Def1;
hence x in C * by A1, Th45; :: thesis: verum

end;