let M be Pnet; ( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of 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 R1 = (Flow M) | the carrier of M;
set S1 = ((Flow M) ~) | the carrier of M;
set T1 = id the carrier of M;
A1:
dom ((Flow M) | the carrier' of M) c= the carrier' of M
by RELAT_1:58;
A2:
rng ((Flow M) | the carrier' of M) c= the carrier of M
by Th9;
A3:
dom (((Flow M) ~) | the carrier' of M) c= the carrier' of M
by RELAT_1:58;
A4:
rng (((Flow M) ~) | the carrier' of M) c= the carrier of M
by Th9;
A5:
dom ((Flow M) | the carrier of M) c= the carrier of M
by RELAT_1:58;
A6:
rng ((Flow M) | the carrier of M) c= the carrier' of M
by Th9;
A7:
dom (((Flow M) ~) | the carrier of M) c= the carrier of M
by RELAT_1:58;
A8:
rng (((Flow M) ~) | the carrier of M) c= the carrier' of M
by Th9;
the carrier of M misses the carrier' of M
by NET_1:def 2;
hence
( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) )
by A1, A2, A3, A4, A5, A6, A7, A8, XBOOLE_1:64; verum