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 Lm4; :: thesis: verum