set f = Cl_Seq T;
for A being Subset of T holds (Cl_Seq T) . ((Cl_Seq T) . A) = (Cl_Seq T) . A

proof

let A be Subset of T; :: thesis: (Cl_Seq T) . ((Cl_Seq T) . A) = (Cl_Seq T) . A
(Cl_Seq T) . ((Cl_Seq T) . A) = (Cl_Seq T) . (Cl_Seq A) by SeqDef
.= Cl_Seq (Cl_Seq A) by SeqDef
.= Cl_Seq A by FRECHET2:21
.= (Cl_Seq T) . A by SeqDef ;
hence (Cl_Seq T) . ((Cl_Seq T) . A) = (Cl_Seq T) . A ; :: thesis: verum

end;

then A1: Cl_Seq T is idempotent ;
Cl_Seq T is preclosure ;
hence Cl_Seq T is closure by A1; :: thesis: verum