let M be Pnet; :: thesis: ( () * () = f_prox 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
.= f_prox M ;
A9: (() \ (id ())) * () = {} \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (id the carrier of M)) by
.= (((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 ;
(() \/ (() ~)) \/ (id ()) = ((Flow M) \/ ((Flow M) ~)) \/ ((id the carrier of M) \/ (id ())) by
.= ((Flow M) \/ ((Flow M) ~)) \/ (id ()) by
.= ((Flow M) \/ (id ())) \/ (((Flow M) ~) \/ (id ())) by XBOOLE_1:5
.= ((Flow M) \/ (id ())) \/ (((Flow M) ~) \/ ((id ()) ~))
.= () \/ (() ~) by RELAT_1:23 ;
hence ( (f_prox M) * () = f_prox M & (() \ (id ())) * () = {} & (() \/ (() ~)) \/ (id ()) = () \/ (() ~) ) by A8, A9; :: thesis: verum