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