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