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