let M be Pnet; ( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~ )) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation 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 Th19
.=
((Flow M) | the carrier' of M) \/ (((Flow M) ~ ) | the carrier' of M)
by Th19
;
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:51
.=
((((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:20
.=
((((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:20
.=
({} \/ ((((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 Th16
.=
({} \/ {} ) \/ ((((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 Th16
.=
({} \/ {} ) \/ ({} \/ ((((Flow M) ~ ) | the carrier' of M) * (((Flow M) ~ ) | the carrier' of M)))
by Th16
.=
{}
by Th16
;
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 Th20
.=
Flow M
by Th21
;
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 Th20
.=
(Flow M) ~
by Th21
;
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:40
.=
((((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_adjac M) \/ ((f_adjac 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:40
.=
(((((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))
by RELAT_1:72
.=
((Flow M) \/ ((Flow M) ~ )) \/ (id the carrier' of M)
by A5
;
A7:
id the carrier' of M c= id (Elements M)
by SYSREL:33, XBOOLE_1:7;
A8: (f_adjac M) * (f_adjac 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:51
.=
((((((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:51
.=
((((((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:20
.=
((((((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:20
.=
((((((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:20
.=
((((((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:20
.=
((((((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:20
.=
((((((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:20
.=
((({} \/ ((((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 Th16
.=
((({} \/ {} ) \/ ((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 Th16
.=
((({} \/ {} ) \/ ((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 Th16
.=
(((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 Th16
.=
(((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 Th17
.=
(((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 Th17
.=
(((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:29
.=
(((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 Th17
.=
(((Flow M) | the carrier' of M) \/ (((Flow M) ~ ) | the carrier' of M)) \/ ({} \/ (id the carrier' of M))
by Th17
.=
f_adjac M
;
A9: ((f_adjac M) \ (id (Elements M))) * (f_adjac M) =
{} \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~ ) | the carrier' of M)) * (id the carrier' of M))
by A1, A2, RELAT_1:51
.=
(((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~ ) | the carrier' of M) * (id the carrier' of M))
by SYSREL:20
.=
{} \/ ((((Flow M) ~ ) | the carrier' of M) * (id the carrier' of M))
by Th17
.=
{}
by Th17
;
((f_adjac M) \/ ((f_adjac 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)) ~ ))
by RELAT_1:72
.=
(f_circulation M) \/ ((f_circulation M) ~ )
by RELAT_1:40
;
hence
( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~ )) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~ ) )
by A8, A9; verum