let M be Pnet; :: thesis: ( () * () = f_adjac M & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) )
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 ();
A1: ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) \ (id ()) = ((((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M))) \ (id ()) by XBOOLE_1:5
.= ((((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ())) \/ (((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ())) by XBOOLE_1:42
.= ((Flow M) | the carrier' of M) \/ (((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ())) 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 ;
A6: () \/ (() ~) = ((((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 () by ;
A8: () * () = (((((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