let T be non empty RelStr ; :: thesis: for A being Subset of holds Fdfl A,2 = (A ^d ) ^d
let A be Subset of ; :: 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