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