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