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