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