let T be non empty RelStr ; for A being Subset of T
for n being Nat holds (Fcl ((A `),n)) ` = Fint (A,n)
let A be Subset of T; for n being Nat holds (Fcl ((A `),n)) ` = Fint (A,n)
let n be Nat; (Fcl ((A `),n)) ` = Fint (A,n)
Fint (A,n) =
((Fint (((A `) `),n)) `) `
.=
(Fcl ((A `),n)) `
by Th27
;
hence
(Fcl ((A `),n)) ` = Fint (A,n)
; verum