let M be Pnet; :: thesis: ( (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M & (the Flow of M | the Transitions of M) \/ (the Flow of M | the Places of M) = the Flow of M & ((the Flow of M | the Places of M) ~ ) \/ ((the Flow of M | the Transitions of M) ~ ) = the Flow of M ~ & ((the Flow of M | the Transitions of M) ~ ) \/ ((the Flow of M | the Places of M) ~ ) = the Flow of M ~ )
set R = the Flow of M;
the Flow of M c= [:(Elements M),(Elements M):] by Th13;
then (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M by SYSREL:25;
hence ( (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M & (the Flow of M | the Transitions of M) \/ (the Flow of M | the Places of M) = the Flow of M & ((the Flow of M | the Places of M) ~ ) \/ ((the Flow of M | the Transitions of M) ~ ) = the Flow of M ~ & ((the Flow of M | the Transitions of M) ~ ) \/ ((the Flow of M | the Places of M) ~ ) = the Flow of M ~ ) by RELAT_1:40; :: thesis: verum