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

assume
S is void
; :: thesis: {} is Subset of Sdefpred S_{1}[ 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_{1}[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 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

hence { v where v is SortSymbol of S : v is with_const_op } is Subset of S ; :: thesis: verum

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