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
(Fcl A) . 0 = A by Def2;
then (Fcl A) . (0 + 1) = A ^b by Def2;
hence Fcl (A,1) = A ^b ; :: thesis: verum