let N be e_net; :: thesis: ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )

A1: (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)

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

.= {} by Th27, RELAT_1:43 ;

(id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)

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

.= {} by Th27, RELAT_1:43 ;

hence ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; :: thesis: verum

A1: (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)

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

.= {} by Th27, RELAT_1:43 ;

(id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)

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

.= {} by Th27, RELAT_1:43 ;

hence ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; :: thesis: verum