let N be e_net; :: thesis: ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )

set R = the entrance of N;

set S = the escape of N;

set T = id the carrier of N;

A1: ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = ((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the escape of N \/ the entrance of N)) \/ (id the carrier of N) by RELAT_1:23

.= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ the escape of N) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4

.= ((( the entrance of N ~) \/ (( the escape of N ~) \/ the escape of N)) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4

.= (( the entrance of N ~) \/ (( the escape of N \/ ( the escape of N ~)) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4

.= (( the entrance of N ~) \/ ( the escape of N \/ (( the escape of N ~) \/ the entrance of N))) \/ (id the carrier of N) by XBOOLE_1:4

.= ((( the entrance of N ~) \/ the escape of N) \/ (( the escape of N ~) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4

.= (e_flow N) \/ ((( the escape of N ~) \/ (( the entrance of N ~) ~)) \/ (id the carrier of N)) by XBOOLE_1:5

.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ (id the carrier of N)) by RELAT_1:23

.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~))

.= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ;

A2: ((e_prox N) \ (id the carrier of N)) * (e_prox N) = ((( the entrance of N ~) \/ ( the escape of N ~)) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) ~) by RELAT_1:23

.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) ~) by XBOOLE_1:42

.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N ~) \/ ( the escape of N ~)) by RELAT_1:23

.= (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the entrance of N ~)) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by RELAT_1:32

.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by SYSREL:6

.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) by SYSREL:6

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:24

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by RELAT_1:35

.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by Def2

.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Def2

.= (({} ~) \/ ({} ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Th15

.= {} by Th15 ;

(e_prox N) * (e_prox N) = (( the entrance of N \/ the escape of N) * ( the entrance of N \/ the escape of N)) ~ by RELAT_1:35

.= ((( the entrance of N \/ the escape of N) * the entrance of N) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by RELAT_1:32

.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by SYSREL:6

.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by SYSREL:6

.= (( the entrance of N \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ the escape of N)) ~ by Def1

.= e_prox N ;

hence ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A2, A1; :: thesis: verum

set R = the entrance of N;

set S = the escape of N;

set T = id the carrier of N;

A1: ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = ((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the escape of N \/ the entrance of N)) \/ (id the carrier of N) by RELAT_1:23

.= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ the escape of N) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4

.= ((( the entrance of N ~) \/ (( the escape of N ~) \/ the escape of N)) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4

.= (( the entrance of N ~) \/ (( the escape of N \/ ( the escape of N ~)) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4

.= (( the entrance of N ~) \/ ( the escape of N \/ (( the escape of N ~) \/ the entrance of N))) \/ (id the carrier of N) by XBOOLE_1:4

.= ((( the entrance of N ~) \/ the escape of N) \/ (( the escape of N ~) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4

.= (e_flow N) \/ ((( the escape of N ~) \/ (( the entrance of N ~) ~)) \/ (id the carrier of N)) by XBOOLE_1:5

.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ (id the carrier of N)) by RELAT_1:23

.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~))

.= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ;

A2: ((e_prox N) \ (id the carrier of N)) * (e_prox N) = ((( the entrance of N ~) \/ ( the escape of N ~)) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) ~) by RELAT_1:23

.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) ~) by XBOOLE_1:42

.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N ~) \/ ( the escape of N ~)) by RELAT_1:23

.= (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the entrance of N ~)) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by RELAT_1:32

.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by SYSREL:6

.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) by SYSREL:6

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))

.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24

.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:24

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35

.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by RELAT_1:35

.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by Def2

.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Def2

.= (({} ~) \/ ({} ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Th15

.= {} by Th15 ;

(e_prox N) * (e_prox N) = (( the entrance of N \/ the escape of N) * ( the entrance of N \/ the escape of N)) ~ by RELAT_1:35

.= ((( the entrance of N \/ the escape of N) * the entrance of N) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by RELAT_1:32

.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by SYSREL:6

.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by SYSREL:6

.= (( the entrance of N \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N * the escape of N))) ~ by Def1

.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ the escape of N)) ~ by Def1

.= e_prox N ;

hence ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A2, A1; :: thesis: verum