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