let E be set ; :: thesis: for A, B being Subset of (E ^omega) st A c= B * holds
A * c= B *
let A, B be Subset of (E ^omega); :: thesis: ( A c= B * implies A * c= B * )
assume A1: A c= B * ; :: thesis: A * c= B *
thus A * c= B * :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A * or x in B * )
assume x in A * ; :: thesis: x in B *
then consider n being Nat such that
A2: x in A |^ n by Th41;
A |^ n c= B * by A1, Th59;
hence x in B * by A2; :: thesis: verum
end;