let T be non empty RelStr ; :: thesis: for A being Subset of T holds Finf (A,2) = (A ^f) ^f
let A be Subset of T; :: thesis: Finf (A,2) = (A ^f) ^f
Finf (A,2) = Finf (A,(1 + 1))
.= (Finf (A,1)) ^f by Def6
.= (A ^f) ^f by Th33 ;
hence Finf (A,2) = (A ^f) ^f ; :: thesis: verum