let R be non empty well-unital multLoopStr ; :: thesis: for X being Subset of R st X in Classes R holds
not X is empty
let X be Subset of R; :: thesis: ( X in Classes R implies not X is empty )
assume X in Classes R ; :: thesis: not X is empty
then ex a being Element of R st X = Class a by Def6;
hence not X is empty ; :: thesis: verum