let A, B be complex-membered set ; :: thesis: for a being Complex holds
( A c= B iff a -- A c= a -- B )
let a be Complex; :: thesis: ( A c= B iff a -- A c= a -- B )
thus ( A c= B implies a -- A c= a -- B ) by Th67; :: thesis: ( a -- A c= a -- B implies A c= B )
assume A1: a -- A c= a -- B ; :: 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 a - z in a -- A by Th160;
then ex c being Complex st
( a - z = a - c & c in B ) by A1, Th162;
hence z in B ; :: thesis: verum