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 }

proof

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;

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

proof

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;

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;
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

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;

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

proof

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;

then { ((B . k) `) where k is Element of NAT : n <= k } = COMPLEMENT Y1 by A8, XBOOLE_0:def 10;
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