@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix log: <http://www.w3.org/2000/10/swap/log.n3#>.
@prefix dpo:  <http://www.daml.org/2001/03/daml+oil#> .
@prefix : <http://www.w3.org/2001/03swell/finiteSet#>.
@prefix v: <#>.
:instance dpo:inverseOf rdf:type.


#@@ slows down figure; commenting out.
#hmm... separate rules?
#<> log:forAll v:x, v:C.
#{ v:x a [ a [ :setOf v:C ] ]} log:implies { v:x a v:C }. #iff rule?@@

#@@split to thm...
# a theorem: if X subset Y, then PowerSet(X) subset PowerSet(Y)
<> log:forAll v:E1, v:E2, v:C1, v:C2, v:P, v:Q.

{ v:C1 :setOf v:E1 }
   log:means { v:C1 dpo:onProperty :_instance; dpo:toClass v:E1 }.

{ v:C1 is :setOf of v:E1.
  v:C2 is :setOf of v:E2.
  v:E1 rdfs:subClassOf v:E2. }
  log:implies { v:C1 rdfs:subClassOf v:C2. }.