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 = (Flow M) | the carrier of M;
set S = ((Flow M) ~) | the carrier of M;
set T = id the carrier of M;
set Q = id (Elements M);
A1: ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \ (id (Elements M)) =
((((Flow M) | the carrier of M) \/ (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M))) \ (id (Elements M))
by XBOOLE_1:5
.=
((((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M))) \/ (((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)))
by XBOOLE_1:42
.=
((Flow M) | the carrier of M) \/ (((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)))
by Th14
.=
((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)
by Th14
;
A2: (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) =
((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * ((Flow M) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M))
by RELAT_1:32
.=
((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M))
by SYSREL:6
.=
((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)))
by SYSREL:6
.=
({} \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)))
by Th11
.=
({} \/ {}) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)))
by Th11
.=
({} \/ {}) \/ ({} \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)))
by Th11
.=
{}
by Th11
;
A3: ((Flow M) | the carrier of M) \/ ((((Flow M) ~) | the carrier of M) ~) =
((Flow M) | the carrier of M) \/ ((((Flow M) | the carrier' of M) ~) ~)
by Th15
.=
Flow M
by Th16
;
A4: (((Flow M) | the carrier of M) ~) \/ (((Flow M) ~) | the carrier of M) =
(((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~)
by Th15
.=
(Flow M) ~
by Th16
;
A5: ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~) \/ (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) =
((((Flow M) | the carrier of M) ~) \/ ((((Flow M) ~) | the carrier of M) ~)) \/ (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M))
by RELAT_1:23
.=
((((Flow M) | the carrier of M) ~) \/ ((((Flow M) ~) | the carrier of M) \/ ((Flow M) | the carrier of M))) \/ ((((Flow M) ~) | the carrier of M) ~)
by XBOOLE_1:4
.=
(((((Flow M) | the carrier of M) ~) \/ (((Flow M) ~) | the carrier of M)) \/ ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) ~)
by XBOOLE_1:4
.=
(Flow M) \/ ((Flow M) ~)
by A3, A4, XBOOLE_1:4
;
A6: (f_prox M) \/ ((f_prox M) ~) =
((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~) \/ ((id the carrier of M) ~))
by RELAT_1:23
.=
(((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) ~)
by XBOOLE_1:4
.=
(((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ (id the carrier of M)) \/ ((id the carrier of M) ~)
by XBOOLE_1:4
.=
((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) \/ ((id the carrier of M) ~))
by XBOOLE_1:4
.=
((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) \/ (id the carrier of M))
.=
((Flow M) \/ ((Flow M) ~)) \/ (id the carrier of M)
by A5
;
A7:
id the carrier of M c= id (Elements M)
by SYSREL:15, XBOOLE_1:7;
A8: (f_prox M) * (f_prox M) =
(((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by RELAT_1:32
.=
((((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * ((Flow M) | the carrier of M)) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by RELAT_1:32
.=
((((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * ((Flow M) | the carrier of M)) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by SYSREL:6
.=
((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by SYSREL:6
.=
((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by SYSREL:6
.=
((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M))
by SYSREL:6
.=
((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (id the carrier of M)) \/ ((id the carrier of M) * (id the carrier of M)))
by SYSREL:6
.=
((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by SYSREL:6
.=
((({} \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th11
.=
((({} \/ {}) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th11
.=
((({} \/ {}) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (({} \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th11
.=
(((id the carrier of M) * ((Flow M) | the carrier of M)) \/ ({} \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th11
.=
(((Flow M) | the carrier of M) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th12
.=
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M)))
by Th12
.=
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ (id the carrier of M))
by SYSREL:12
.=
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (({} \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ (id the carrier of M))
by Th12
.=
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier of M))
by Th12
.=
f_prox M
;
A9: ((f_prox M) \ (id (Elements M))) * (f_prox M) =
{} \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (id the carrier of M))
by A1, A2, RELAT_1:32
.=
(((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))
by SYSREL:6
.=
{} \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))
by Th12
.=
{}
by Th12
;
((f_prox M) \/ ((f_prox M) ~)) \/ (id (Elements M)) =
((Flow M) \/ ((Flow M) ~)) \/ ((id the carrier of M) \/ (id (Elements M)))
by A6, XBOOLE_1:4
.=
((Flow M) \/ ((Flow M) ~)) \/ (id (Elements M))
by A7, XBOOLE_1:12
.=
((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ (id (Elements M)))
by XBOOLE_1:5
.=
((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ ((id (Elements M)) ~))
.=
(f_flow M) \/ ((f_flow M) ~)
by RELAT_1:23
;
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