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

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