1		package(load_event_b_project([],[event_b_context(none,'KuratowskiPairDefinition_Enum',[extends(none,['KuratowskiPairDefinition']),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('KuratowskiPairDefinition_Enum',part,'_6zVcMXmcEeWc79uavmneRQ'),identifier(none,'S1'),[set_extension(none,[identifier(none,a)]),set_extension(none,[identifier(none,b)]),set_extension(none,[identifier(none,c)])])]),theorems(none,[]),sets(none,[])]),event_b_context(none,'KuratowskiPairDefinition',[extends(none,[]),constants(none,[identifier(none,u),identifier(none,v),identifier(none,x),identifier(none,y)]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos('KuratowskiPairDefinition',axm1,'_GcE2ZnmcEeWc79uavmneRQ'),member(none,identifier(none,x),identifier(none,'S1')),member(none,identifier(none,y),identifier(none,'S1'))),conjunct(rodinpos('KuratowskiPairDefinition',axm2,'_GcFdcHmcEeWc79uavmneRQ'),member(none,identifier(none,u),identifier(none,'S1')),member(none,identifier(none,v),identifier(none,'S1')))]),theorems(none,[equivalence(rodinpos('KuratowskiPairDefinition',pair1,'_GcFdcXmcEeWc79uavmneRQ'),equal(none,couple(none,[identifier(none,x),identifier(none,y)]),couple(none,[identifier(none,u),identifier(none,v)])),conjunct(none,equal(none,identifier(none,x),identifier(none,u)),equal(none,identifier(none,y),identifier(none,v)))),equivalence(rodinpos('KuratowskiPairDefinition',pair2,'_GcFdcnmcEeWc79uavmneRQ'),equal(none,set_extension(none,[set_extension(none,[identifier(none,x)]),set_extension(none,[identifier(none,x),identifier(none,y)])]),set_extension(none,[set_extension(none,[identifier(none,u)]),set_extension(none,[identifier(none,u),identifier(none,v)])])),conjunct(none,equal(none,identifier(none,x),identifier(none,u)),equal(none,identifier(none,y),identifier(none,v)))),equivalence(rodinpos('KuratowskiPairDefinition',pair3,'_oN5LEHmcEeWc79uavmneRQ'),equal(none,set_extension(none,[set_extension(none,[set_extension(none,[identifier(none,x)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'S1')))]),set_extension(none,[set_extension(none,[identifier(none,y)])])]),set_extension(none,[set_extension(none,[set_extension(none,[identifier(none,u)]),typeof(none,empty_set(none),pow_subset(none,identifier(none,'S1')))]),set_extension(none,[set_extension(none,[identifier(none,v)])])])),conjunct(none,equal(none,identifier(none,x),identifier(none,u)),equal(none,identifier(none,y),identifier(none,v))))]),sets(none,[deferred_set(none,'S1'),deferred_set(none,'S2')])])],[exporter_version(3),po('KuratowskiPairDefinition','Theorem',[axiom(pair1)],true),po('KuratowskiPairDefinition','Theorem',[axiom(pair2)],false),po('KuratowskiPairDefinition','Theorem',[axiom(pair3)],false)],_Error)).
2