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