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
A1: ( ( for n being Element of NAT
for B being Subset of T st B = (Finf A) . n holds
(Finf A) . (n + 1) = B ^f ) & (Finf A) . 0 = A ) by Def6;
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 by A1; :: thesis: verum