let n be Element of NAT ; :: thesis: for X being set
for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
let X be set ; :: thesis: for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
let B be SetSequence of X; :: thesis: (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) `
reconsider Y = (inferior_setsequence (Complement B)) . n as Subset of X ;
Y = ((superior_setsequence (Complement (Complement B))) . n) ` by Th30
.= ((superior_setsequence B) . n) ` ;
hence (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` ; :: thesis: verum