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