let M be Pnet; :: thesis: ( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} )
A1: (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M

proof

rng (the Flow of M | the Transitions of M) c= the Places of M by Th14;
hence (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M by RELAT_1:79; :: thesis: verum

end;

A2: ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M

proof

rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M by Th14;
hence ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M by RELAT_1:79; :: thesis: verum

end;

A3: (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M

proof

dom (the Flow of M | the Transitions of M) c= the Transitions of M by RELAT_1:87;
hence (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M by RELAT_1:77; :: thesis: verum

end;

A4: (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M

proof

dom ((the Flow of M ~ ) | the Transitions of M) c= the Transitions of M by RELAT_1:87;
hence (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M by RELAT_1:77; :: thesis: verum

end;

A5: (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M

proof

rng (the Flow of M | the Places of M) c= the Transitions of M by Th14;
hence (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M by RELAT_1:79; :: thesis: verum

end;

A6: ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M

proof

rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M by Th14;
hence ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M by RELAT_1:79; :: thesis: verum

end;

A7: (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M

proof

dom (the Flow of M | the Places of M) c= the Places of M by RELAT_1:87;
hence (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M by RELAT_1:77; :: thesis: verum

end;

A8: (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M

proof

dom ((the Flow of M ~ ) | the Places of M) c= the Places of M by RELAT_1:87;
hence (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M by RELAT_1:77; :: thesis: verum

end;

A9: (id the Transitions of M) * (the Flow of M | the Places of M) = {}

proof

dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) by Th15;
hence (id the Transitions of M) * (the Flow of M | the Places of M) = {} by RELAT_1:67; :: thesis: verum

end;

A10: (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {}

proof

dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) by Th15;
hence (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} by RELAT_1:67; :: thesis: verum

end;

A11: (the Flow of M | the Places of M) * (id the Places of M) = {}

proof

rng (the Flow of M | the Places of M) misses dom (id the Places of M) by Th15;
hence (the Flow of M | the Places of M) * (id the Places of M) = {} by RELAT_1:67; :: thesis: verum

end;

A12: ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {}

proof

rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) by Th15;
hence ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} by RELAT_1:67; :: thesis: verum

end;

A13: (id the Places of M) * (the Flow of M | the Transitions of M) = {}

proof

rng (id the Places of M) misses dom (the Flow of M | the Transitions of M) by Th15;
hence (id the Places of M) * (the Flow of M | the Transitions of M) = {} by RELAT_1:67; :: thesis: verum

end;

A14: (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {}

proof

rng (id the Places of M) misses dom ((the Flow of M ~ ) | the Transitions of M) by Th15;
hence (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} by RELAT_1:67; :: thesis: verum

end;

A15: (the Flow of M | the Transitions of M) * (id the Transitions of M) = {}

proof

rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) by Th15;
hence (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} by RELAT_1:67; :: thesis: verum

end;

((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {}

proof

rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) by Th15;
hence ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} by RELAT_1:67; :: thesis: verum

end;

hence ( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15; :: thesis: verum