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