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

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

end;

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