let X be set ; :: thesis: for B being SetSequence of X

for n being Element of NAT holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

let B be SetSequence of X; :: thesis: for n being Element of NAT holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

let n be Element of NAT ; :: thesis: (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

set Y1 = { (B . k1) where k1 is Nat : n <= k1 } ;

set Y2 = { ((Complement B) . k2) where k2 is Nat : n <= k2 } ;

set Y3 = { ((B . k) `) where k is Element of NAT : n <= k } ;

A1: { ((B . k) `) where k is Element of NAT : n <= k } c= { ((Complement B) . k2) where k2 is Nat : n <= k2 }

A7: { (B . k1) where k1 is Nat : n <= k1 } <> {} by Th1;

reconsider Y1 = { (B . k1) where k1 is Nat : n <= k1 } as Subset-Family of X by Th28;

A8: COMPLEMENT Y1 c= { ((B . k) `) where k is Element of NAT : n <= k }

then (superior_setsequence (Complement B)) . n = union (COMPLEMENT Y1) by A6, Def3

.= ([#] X) \ (meet Y1) by A7, SETFAM_1:34

.= (meet Y1) ` ;

hence (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` by Def2; :: thesis: verum

for n being Element of NAT holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

let B be SetSequence of X; :: thesis: for n being Element of NAT holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

let n be Element of NAT ; :: thesis: (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `

set Y1 = { (B . k1) where k1 is Nat : n <= k1 } ;

set Y2 = { ((Complement B) . k2) where k2 is Nat : n <= k2 } ;

set Y3 = { ((B . k) `) where k is Element of NAT : n <= k } ;

A1: { ((B . k) `) where k is Element of NAT : n <= k } c= { ((Complement B) . k2) where k2 is Nat : n <= k2 }

proof

{ ((Complement B) . k2) where k2 is Nat : n <= k2 } c= { ((B . k) `) where k is Element of NAT : n <= k }
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { ((B . k) `) where k is Element of NAT : n <= k } or y in { ((Complement B) . k2) where k2 is Nat : n <= k2 } )

assume y in { ((B . k) `) where k is Element of NAT : n <= k } ; :: thesis: y in { ((Complement B) . k2) where k2 is Nat : n <= k2 }

then consider k being Element of NAT such that

A2: y = (B . k) ` and

A3: n <= k ;

y = (Complement B) . k by A2, PROB_1:def 2;

hence y in { ((Complement B) . k2) where k2 is Nat : n <= k2 } by A3; :: thesis: verum

end;assume y in { ((B . k) `) where k is Element of NAT : n <= k } ; :: thesis: y in { ((Complement B) . k2) where k2 is Nat : n <= k2 }

then consider k being Element of NAT such that

A2: y = (B . k) ` and

A3: n <= k ;

y = (Complement B) . k by A2, PROB_1:def 2;

hence y in { ((Complement B) . k2) where k2 is Nat : n <= k2 } by A3; :: thesis: verum

proof

then A6:
{ ((Complement B) . k2) where k2 is Nat : n <= k2 } = { ((B . k) `) where k is Element of NAT : n <= k }
by A1, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((Complement B) . k2) where k2 is Nat : n <= k2 } or x in { ((B . k) `) where k is Element of NAT : n <= k } )

assume x in { ((Complement B) . k2) where k2 is Nat : n <= k2 } ; :: thesis: x in { ((B . k) `) where k is Element of NAT : n <= k }

then consider k being Nat such that

A4: x = (Complement B) . k and

A5: n <= k ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

x = (B . k) ` by A4, PROB_1:def 2;

hence x in { ((B . k) `) where k is Element of NAT : n <= k } by A5; :: thesis: verum

end;assume x in { ((Complement B) . k2) where k2 is Nat : n <= k2 } ; :: thesis: x in { ((B . k) `) where k is Element of NAT : n <= k }

then consider k being Nat such that

A4: x = (Complement B) . k and

A5: n <= k ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

x = (B . k) ` by A4, PROB_1:def 2;

hence x in { ((B . k) `) where k is Element of NAT : n <= k } by A5; :: thesis: verum

A7: { (B . k1) where k1 is Nat : n <= k1 } <> {} by Th1;

reconsider Y1 = { (B . k1) where k1 is Nat : n <= k1 } as Subset-Family of X by Th28;

A8: COMPLEMENT Y1 c= { ((B . k) `) where k is Element of NAT : n <= k }

proof

{ ((B . k) `) where k is Element of NAT : n <= k } c= COMPLEMENT Y1
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in COMPLEMENT Y1 or y in { ((B . k) `) where k is Element of NAT : n <= k } )

assume A9: y in COMPLEMENT Y1 ; :: thesis: y in { ((B . k) `) where k is Element of NAT : n <= k }

then reconsider y = y as Subset of X ;

y ` in Y1 by A9, SETFAM_1:def 7;

then consider k being Nat such that

A10: y ` = B . k and

A11: n <= k ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

y = (B . k) ` by A10;

hence y in { ((B . k) `) where k is Element of NAT : n <= k } by A11; :: thesis: verum

end;assume A9: y in COMPLEMENT Y1 ; :: thesis: y in { ((B . k) `) where k is Element of NAT : n <= k }

then reconsider y = y as Subset of X ;

y ` in Y1 by A9, SETFAM_1:def 7;

then consider k being Nat such that

A10: y ` = B . k and

A11: n <= k ;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

y = (B . k) ` by A10;

hence y in { ((B . k) `) where k is Element of NAT : n <= k } by A11; :: thesis: verum

proof

then
{ ((B . k) `) where k is Element of NAT : n <= k } = COMPLEMENT Y1
by A8, XBOOLE_0:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((B . k) `) where k is Element of NAT : n <= k } or x in COMPLEMENT Y1 )

assume x in { ((B . k) `) where k is Element of NAT : n <= k } ; :: thesis: x in COMPLEMENT Y1

then consider k being Element of NAT such that

A12: x = (B . k) ` and

A13: n <= k ;

reconsider z = B . k as Subset of X ;

(z `) ` in Y1 by A13;

hence x in COMPLEMENT Y1 by A12, SETFAM_1:def 7; :: thesis: verum

end;assume x in { ((B . k) `) where k is Element of NAT : n <= k } ; :: thesis: x in COMPLEMENT Y1

then consider k being Element of NAT such that

A12: x = (B . k) ` and

A13: n <= k ;

reconsider z = B . k as Subset of X ;

(z `) ` in Y1 by A13;

hence x in COMPLEMENT Y1 by A12, SETFAM_1:def 7; :: thesis: verum

then (superior_setsequence (Complement B)) . n = union (COMPLEMENT Y1) by A6, Def3

.= ([#] X) \ (meet Y1) by A7, SETFAM_1:34

.= (meet Y1) ` ;

hence (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` by Def2; :: thesis: verum