let A, B be complex-membered set ; :: thesis: ( A c= B implies A "" c= B "" )
assume A1: A c= B ; :: thesis: A "" c= B ""
let a be Complex; :: according to MEMBERED:def 7 :: thesis: ( not a in A "" or a in B "" )
assume a in A "" ; :: thesis: a in B ""
then a " in A by Th29;
hence a in B "" by A1, Th29; :: thesis: verum