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

proof

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

end;

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