consider Y being Field_Subset of X such that
A1: Y = meet { Z where Z is Field_Subset of X : S c= Z } by ExistAlgebra;
thus meet { Z where Z is Field_Subset of X : S c= Z } is Field_Subset of X by A1; :: thesis: verum