let E be set ; :: thesis: for A, B, C 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, B, C 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:17;
hence A ^^ B c= C |^ (k + l) by FLANG_1:33; :: thesis: verum