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 Th12;
hence a in -- B by A1, Th12; :: thesis: verum