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