let M be Pnet; ( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~ ) )
set R = the Flow of M | the Places of M;
set S = (the Flow of M ~ ) | the Places of M;
set T = id the Places of M;
set Q = id (Elements M);
A1: (((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) \/ (id the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M))) \ (id (Elements M))
by XBOOLE_1:5
.=
(((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 the Places of M)) \ (id (Elements M)))
by XBOOLE_1:42
.=
(the Flow of M | the Places of M) \/ ((((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)))
by Th19
.=
(the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)
by Th19
;
A2: ((the Flow of M | 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)) =
(((the Flow of M | 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) \/ ((the Flow of M ~ ) | the Places of M)) * ((the Flow of M ~ ) | the Places of M))
by RELAT_1:51
.=
(((the Flow of M | 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))) \/ (((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) * ((the Flow of M ~ ) | the Places of M))
by SYSREL:20
.=
(((the Flow of M | 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))) \/ (((the Flow of M | 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)))
by SYSREL:20
.=
({} \/ (((the Flow of M ~ ) | 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)) \/ (((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M)))
by Th16
.=
({} \/ {} ) \/ (((the Flow of M | 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)))
by Th16
.=
({} \/ {} ) \/ ({} \/ (((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M)))
by Th16
.=
{}
by Th16
;
A3: (the Flow of M | 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 Transitions of M) ~ ) ~ )
by Th20
.=
the Flow of M
by Th21
;
A4: ((the Flow of M | 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 Transitions of M) ~ )
by Th20
.=
the Flow of M ~
by Th21
;
A5: (((the Flow of M | 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)) =
(((the Flow of M | 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))
by RELAT_1:40
.=
(((the Flow of M | 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) ~ )
by XBOOLE_1:4
.=
((((the Flow of M | 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) ~ )
by XBOOLE_1:4
.=
the Flow of M \/ (the Flow of M ~ )
by A3, A4, XBOOLE_1:4
;
A6: (f_prox M) \/ ((f_prox 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)) ~ ) \/ ((id the Places of M) ~ ))
by RELAT_1:40
.=
((((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)) ~ )) \/ ((id the Places of M) ~ )
by XBOOLE_1:4
.=
((((the Flow of M | 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 Places of M)) \/ ((id the Places of M) ~ )
by XBOOLE_1:4
.=
(((the Flow of M | 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 Places of M) \/ ((id the Places of M) ~ ))
by XBOOLE_1:4
.=
(((the Flow of M | 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 Places of M) \/ (id the Places of M))
by RELAT_1:72
.=
(the Flow of M \/ (the Flow of M ~ )) \/ (id the Places of M)
by A5
;
A7:
id the Places of M c= id (Elements M)
by SYSREL:33, XBOOLE_1:7;
A8: (f_prox M) * (f_prox 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) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M)) * (id the Places of M))
by RELAT_1:51
.=
(((((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 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 Places of M)) * (id the Places of M))
by RELAT_1:51
.=
(((((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 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 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 Places of M)) * (id the Places of M))
by SYSREL:20
.=
(((((the Flow of M | 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 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 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 Places of M)) * (id the Places of M))
by SYSREL:20
.=
(((((the Flow of M | 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 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)) * ((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 Places of M)) * (id the Places of M))
by SYSREL:20
.=
(((((the Flow of M | 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 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)) \/ (((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 Places of M)) * (id the Places of M))
by SYSREL:20
.=
(((((the Flow of M | 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 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)) \/ (((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 Places of M)) \/ ((id the Places of M) * (id the Places of M)))
by SYSREL:20
.=
(((((the Flow of M | 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 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)) \/ (((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) * (id the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by SYSREL:20
.=
((({} \/ (((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)) \/ (((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) * (id the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th16
.=
((({} \/ {} ) \/ ((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)) \/ (((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) * (id the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th16
.=
((({} \/ {} ) \/ ((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 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) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th16
.=
(((id 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) * (id the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th16
.=
((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) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th17
.=
((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 Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ ((id the Places of M) * (id the Places of M)))
by Th17
.=
((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 Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))) \/ (id the Places of M))
by SYSREL:29
.=
((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 Places of M))) \/ (id the Places of M))
by Th17
.=
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ ({} \/ (id the Places of M))
by Th17
.=
f_prox M
;
A9: ((f_prox M) \ (id (Elements M))) * (f_prox M) =
{} \/ (((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) * (id the Places of M))
by A1, A2, RELAT_1:51
.=
((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))
by SYSREL:20
.=
{} \/ (((the Flow of M ~ ) | the Places of M) * (id the Places of M))
by Th17
.=
{}
by Th17
;
((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) =
(the Flow of M \/ (the Flow of M ~ )) \/ ((id the Places of M) \/ (id (Elements M)))
by A6, XBOOLE_1:4
.=
(the Flow of M \/ (the Flow of M ~ )) \/ (id (Elements M))
by A7, XBOOLE_1:12
.=
(the Flow of M \/ (id (Elements M))) \/ ((the Flow of M ~ ) \/ (id (Elements M)))
by XBOOLE_1:5
.=
(the Flow of M \/ (id (Elements M))) \/ ((the Flow of M ~ ) \/ ((id (Elements M)) ~ ))
by RELAT_1:72
.=
(f_flow M) \/ ((f_flow M) ~ )
by RELAT_1:40
;
hence
( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~ ) )
by A8, A9; verum