let T be non empty RelStr ; :: thesis: for A being Subset of T holds Fint (A,2) = (A ^i) ^i
let A be Subset of T; :: thesis: Fint (A,2) = (A ^i) ^i
thus Fint (A,2) = Fint (A,(1 + 1))
.= (Fint (A,1)) ^i by Def4
.= (A ^i) ^i by Th20 ; :: thesis: verum