let A, B be complex-membered set ; :: thesis: for a being Complex holds
( A c= B iff A -- a c= B -- a )
let a be Complex; :: thesis: ( A c= B iff A -- a c= B -- a )
thus ( A c= B implies A -- a c= B -- a ) by Th67; :: thesis: ( A -- a c= B -- a implies A c= B )
assume A1: A -- a c= B -- a ; :: thesis: A c= B
let z be Complex; :: according to MEMBERED:def 7 :: thesis: ( not z in A or z in B )
assume z in A ; :: thesis: z in B
then z - a in A -- a by Th176;
then ex c being Complex st
( z - a = c - a & c in B ) by A1, Th178;
hence z in B ; :: thesis: verum