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 that

A1: A c= C + and

A2: B c= C + ; :: thesis: A ^^ B c= C +

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 FLANG_1:def 1;

hence x in C + by A1, A2, Th66; :: thesis: verum

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 that

A1: A c= C + and

A2: B c= C + ; :: thesis: A ^^ B c= C +

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 FLANG_1:def 1;

hence x in C + by A1, A2, Th66; :: thesis: verum