for i being object st i in the carrier of S holds
not (OSClass E) . i is empty

proof

let i be object ; :: thesis: ( i in the carrier of S implies not (OSClass E) . i is empty )
assume i in the carrier of S ; :: thesis: not (OSClass E) . i is empty
then reconsider s = i as Element of S ;
(OSClass E) . s = OSClass (E,s) by Def11;
hence not (OSClass E) . i is empty ; :: thesis: verum

end;

hence OSClass E is non-empty by PBOOLE:def 13; :: thesis: verum