hereby :: thesis: ( S is void implies {} is Subset of )

defpred S₁[ SortSymbol of ] means $1 is with_const_op ;
assume not S is void ; :: thesis: { v where v is SortSymbol of : v is with_const_op } is Subset of
{ v where v is SortSymbol of : S₁[v] } is Subset of from DOMAIN_1:sch 7();
hence { v where v is SortSymbol of : v is with_const_op } is Subset of ; :: thesis: verum

end;

assume S is void ; :: thesis: {} is Subset of
thus {} is Subset of by SUBSET_1:4; :: thesis: verum