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