let X be set ; :: thesis: for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B)
let B be SetSequence of X; :: thesis: Complement (superior_setsequence B) = inferior_setsequence (Complement B)
reconsider A2 = inferior_setsequence (Complement B) as SetSequence of X ;
Complement A2 = superior_setsequence (Complement (Complement B)) by Th32
.= superior_setsequence B ;
hence Complement (superior_setsequence B) = inferior_setsequence (Complement B) ; :: thesis: verum