set f = Cl_Seq T;
z2: (Cl_Seq T) . ({} T) = Cl_Seq ({} T) by SeqDef;
z1: for A, B being Subset of T holds (Cl_Seq T) . (A \/ B) = ((Cl_Seq T) . A) \/ ((Cl_Seq T) . B)
proof
let A, B be Subset of T; :: thesis: (Cl_Seq T) . (A \/ B) = ((Cl_Seq T) . A) \/ ((Cl_Seq T) . B)
(Cl_Seq T) . (A \/ B) = Cl_Seq (A \/ B) by SeqDef
.= (Cl_Seq A) \/ (Cl_Seq B) by FRECHET2:19
.= ((Cl_Seq T) . A) \/ (Cl_Seq B) by SeqDef
.= ((Cl_Seq T) . A) \/ ((Cl_Seq T) . B) by SeqDef ;
hence (Cl_Seq T) . (A \/ B) = ((Cl_Seq T) . A) \/ ((Cl_Seq T) . B) ; :: thesis: verum
end;
for A being Subset of T holds A c= (Cl_Seq T) . A
proof
let A be Subset of T; :: thesis: A c= (Cl_Seq T) . A
A c= Cl_Seq A by FRECHET2:18;
hence A c= (Cl_Seq T) . A by SeqDef; :: thesis: verum
end;
then ( Cl_Seq T is extensive & Cl_Seq T is \/-preserving & Cl_Seq T is empty-preserving ) by z1, z2, FRECHET2:17;
hence Cl_Seq T is preclosure ; :: thesis: verum