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 ;

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

hence
Complement (inferior_setsequence B) = superior_setsequence (Complement B)
by FUNCT_2:63; :: thesis: verumlet 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;(A2 . n) ` = ((A3 . n) `) ` by Th30;

hence (Complement A2) . n = A3 . n by PROB_1:def 2; :: thesis: verum