let T be non empty RelStr ; :: thesis: for A being Subset of T holds Fcl (A,2) = (A ^b) ^b
let A be Subset of T; :: thesis: Fcl (A,2) = (A ^b) ^b
for B being Subset of T st B = (Fcl A) . 1 holds
(Fcl A) . (1 + 1) = B ^b by Def2;
then Fcl (A,2) = (Fcl (A,1)) ^b
.= (A ^b) ^b by Th15 ;
hence Fcl (A,2) = (A ^b) ^b ; :: thesis: verum