let E be set ; :: thesis: for A, C, B being Subset of (E ^omega )
for k, l being Nat st A c= C |^ k & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
let A, C, B be Subset of (E ^omega ); :: thesis: for k, l being Nat st A c= C |^ k & B c= C |^ l holds
A ^^ B c= C |^ (k + l)
let k, l be Nat; :: thesis: ( A c= C |^ k & B c= C |^ l implies A ^^ B c= C |^ (k + l) )
assume ( A c= C |^ k & B c= C |^ l ) ; :: thesis: A ^^ B c= C |^ (k + l)
then A ^^ B c= (C |^ k) ^^ (C |^ l) by FLANG_1:18;
hence A ^^ B c= C |^ (k + l) by FLANG_1:34; :: thesis: verum