:: deftheorem Def2 defines Complement PROB_1:def 2 :
for X being set
for A1, b₃ being SetSequence of X holds
( b₃ = Complement A1 iff for n being Nat holds b₃ . n = (A1 . n) ` );