let X be set ; :: thesis: for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B)
let B be SetSequence of X; :: thesis: Complement (inferior_setsequence B) = superior_setsequence (Complement B)
reconsider A2 = inferior_setsequence B as SetSequence of X ;
reconsider A3 = superior_setsequence (Complement B) as SetSequence of X ;

now :: thesis: for n being Element of NAT holds (Complement A2) . n = A3 . n

let n be Element of NAT ; :: thesis: (Complement A2) . n = A3 . n
(A2 . n) ` = ((A3 . n) `) ` by Th30;
hence (Complement A2) . n = A3 . n by PROB_1:def 2; :: thesis: verum

end;

hence Complement (inferior_setsequence B) = superior_setsequence (Complement B) by FUNCT_2:63; :: thesis: verum