let n be Element of NAT ; :: thesis: for X being set
for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
let X be set ; :: thesis: for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
let B be SetSequence of X; :: thesis: (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) `
set Y1 = { (B . k1) where k1 is Element of NAT : n <= k1 } ;
set Y2 = { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } ;
set Y3 = { ((B . k) ` ) where k is Element of NAT : n <= k } ;
A0: ( { (B . k1) where k1 is Element of NAT : n <= k1 } <> {} & { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } <> {} ) by Th5;
B: { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } = { ((B . k) ` ) where k is Element of NAT : n <= k }

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((Complement B) . k2) where k2 is Element of 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 Element of NAT : n <= k2 } ; :: thesis: x in { ((B . k) ` ) where k is Element of NAT : n <= k }
then consider k being Element of NAT such that
B1: ( x = (Complement B) . k & n <= k ) ;
( x = (B . k) ` & n <= k ) by B1, PROB_1:def 4;
hence x in { ((B . k) ` ) where k is Element of NAT : n <= k } ; :: thesis: verum

end;

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

proof

let y be set ; :: 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 Element of 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 Element of NAT : n <= k2 }
then consider k being Element of NAT such that
B2: ( y = (B . k) ` & n <= k ) ;
( y = (Complement B) . k & n <= k ) by B2, PROB_1:def 4;
hence y in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } ; :: thesis: verum

end;

hence { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } = { ((B . k) ` ) where k is Element of NAT : n <= k } by B01, XBOOLE_0:def 10; :: thesis: verum

end;

reconsider Y1 = { (B . k1) where k1 is Element of NAT : n <= k1 } as Subset-Family of X by Th98;
{ ((B . k) ` ) where k is Element of NAT : n <= k } = COMPLEMENT Y1

proof

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

proof

let x be set ; :: 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
C1: ( x = (B . k) ` & n <= k ) ;
reconsider z = B . k as Subset of X ;
(z ` ) ` in Y1 by C1;
hence x in COMPLEMENT Y1 by C1, SETFAM_1:def 8; :: thesis: verum

end;

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

proof

let y be set ; :: 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 C3: 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 C3, SETFAM_1:def 8;
then consider k being Element of NAT such that
C4: ( y ` = B . k & n <= k ) ;
( y = (B . k) ` & n <= k ) by C4;
hence y in { ((B . k) ` ) where k is Element of NAT : n <= k } ; :: thesis: verum

end;

hence { ((B . k) ` ) where k is Element of NAT : n <= k } = COMPLEMENT Y1 by C01, XBOOLE_0:def 10; :: thesis: verum

end;

then (superior_setsequence (Complement B)) . n = union (COMPLEMENT Y1) by B, def3
.= ([#] X) \ (meet Y1) by A0, SETFAM_1:48
.= (meet Y1) ` ;
hence (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` by def2; :: thesis: verum