let M be Pnet; :: thesis: ( (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M )
A1: (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M
proof
set R = (the Flow of M ~ ) | the Transitions of M;
set S = id the Places of M;
set T = id (Elements M);
A2: id the Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A3: (the Flow of M ~ ) | the Transitions of M misses id (Elements M) by Th18;
(((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (((the Flow of M ~ ) | the Transitions of M) \ (id (Elements M))) \/ ((id the Places of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((the Flow of M ~ ) | the Transitions of M) \ (id (Elements M))) \/ {} by A2, XBOOLE_1:37
.= (the Flow of M ~ ) | the Transitions of M by A3, XBOOLE_1:83 ;
hence (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M ; :: thesis: verum
end;
A4: ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M
proof
set R = the Flow of M | the Transitions of M;
set S = id the Places of M;
set T = id (Elements M);
A5: id the Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A6: the Flow of M | the Transitions of M misses id (Elements M) by Th18;
((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = ((the Flow of M | the Transitions of M) \ (id (Elements M))) \/ ((id the Places of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((the Flow of M | the Transitions of M) \ (id (Elements M))) \/ {} by A5, XBOOLE_1:37
.= the Flow of M | the Transitions of M by A6, XBOOLE_1:83 ;
hence ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M ; :: thesis: verum
end;
A7: (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M
proof
set R = (the Flow of M ~ ) | the Places of M;
set S = id the Places of M;
set T = id (Elements M);
A8: id the Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A9: (the Flow of M ~ ) | the Places of M misses id (Elements M) by Th18;
(((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (((the Flow of M ~ ) | the Places of M) \ (id (Elements M))) \/ ((id the Places of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((the Flow of M ~ ) | the Places of M) \ (id (Elements M))) \/ {} by A8, XBOOLE_1:37
.= (the Flow of M ~ ) | the Places of M by A9, XBOOLE_1:83 ;
hence (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M ; :: thesis: verum
end;
A10: ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M
proof
set R = the Flow of M | the Places of M;
set S = id the Places of M;
set T = id (Elements M);
A11: id the Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A12: the Flow of M | the Places of M misses id (Elements M) by Th18;
((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = ((the Flow of M | the Places of M) \ (id (Elements M))) \/ ((id the Places of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((the Flow of M | the Places of M) \ (id (Elements M))) \/ {} by A11, XBOOLE_1:37
.= the Flow of M | the Places of M by A12, XBOOLE_1:83 ;
hence ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M ; :: thesis: verum
end;
A13: (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M
proof
set R = (the Flow of M ~ ) | the Places of M;
set S = id the Transitions of M;
set T = id (Elements M);
A14: id the Transitions of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A15: (the Flow of M ~ ) | the Places of M misses id (Elements M) by Th18;
(((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (((the Flow of M ~ ) | the Places of M) \ (id (Elements M))) \/ ((id the Transitions of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((the Flow of M ~ ) | the Places of M) \ (id (Elements M))) \/ {} by A14, XBOOLE_1:37
.= (the Flow of M ~ ) | the Places of M by A15, XBOOLE_1:83 ;
hence (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M ; :: thesis: verum
end;
A16: ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M
proof
set R = the Flow of M | the Places of M;
set S = id the Transitions of M;
set T = id (Elements M);
A17: id the Transitions of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A18: the Flow of M | the Places of M misses id (Elements M) by Th18;
((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = ((the Flow of M | the Places of M) \ (id (Elements M))) \/ ((id the Transitions of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((the Flow of M | the Places of M) \ (id (Elements M))) \/ {} by A17, XBOOLE_1:37
.= the Flow of M | the Places of M by A18, XBOOLE_1:83 ;
hence ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M ; :: thesis: verum
end;
A19: (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M
proof
set R = (the Flow of M ~ ) | the Transitions of M;
set S = id the Transitions of M;
set T = id (Elements M);
A20: id the Transitions of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A21: (the Flow of M ~ ) | the Transitions of M misses id (Elements M) by Th18;
(((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (((the Flow of M ~ ) | the Transitions of M) \ (id (Elements M))) \/ ((id the Transitions of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((the Flow of M ~ ) | the Transitions of M) \ (id (Elements M))) \/ {} by A20, XBOOLE_1:37
.= (the Flow of M ~ ) | the Transitions of M by A21, XBOOLE_1:83 ;
hence (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M ; :: thesis: verum
end;
((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M
proof
set R = the Flow of M | the Transitions of M;
set S = id the Transitions of M;
set T = id (Elements M);
A22: id the Transitions of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
A23: the Flow of M | the Transitions of M misses id (Elements M) by Th18;
((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = ((the Flow of M | the Transitions of M) \ (id (Elements M))) \/ ((id the Transitions of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((the Flow of M | the Transitions of M) \ (id (Elements M))) \/ {} by A22, XBOOLE_1:37
.= the Flow of M | the Transitions of M by A23, XBOOLE_1:83 ;
hence ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M ; :: thesis: verum
end;
hence ( (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M ) by A1, A4, A7, A10, A13, A16, A19; :: thesis: verum