let A, B be complex-membered set ; :: thesis: ( A c= B iff A "" c= B "" )
( (A "") "" = A & (B "") "" = B ) ;
hence ( A c= B iff A "" c= B "" ) by Lm3; :: thesis: verum