let E be set ; :: thesis: for A, B being Subset of st A c= B holds
A * c= B *
let A, B be Subset of ; :: thesis: ( A c= B implies A * c= B * )
assume A1: A c= B ; :: thesis: A * c= B *
B c= B * by Th44;
then A c= B * by A1, XBOOLE_1:1;
hence A * c= B * by Th61; :: thesis: verum