consider Y being non empty preBoolean Subset-Family of X such that
A1: Y = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } by ExistRing;
thus meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } is non empty preBoolean Subset-Family of X by A1; :: thesis: verum