let M be Pnet; :: thesis: ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier' of M )
A1: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M
proof
set R = ((Flow M) ~) | the carrier' of M;
set S = id the carrier of M;
set T = id ();
A2: id the carrier of M c= id () by ;
A3: ((Flow M) ~) | the carrier' of M misses id () by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = ((((Flow M) ~) | the carrier' of M) \ (id ())) \/ ((id the carrier of M) \ (id ())) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id ())) \/ {} by
.= ((Flow M) ~) | the carrier' of M by ;
hence ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M ; :: thesis: verum
end;
A4: (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier' of M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = id ();
A5: id the carrier of M c= id () by ;
A6: (Flow M) | the carrier' of M misses id () by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = (((Flow M) | the carrier' of M) \ (id ())) \/ ((id the carrier of M) \ (id ())) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id ())) \/ {} by
.= (Flow M) | the carrier' of M by ;
hence (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier' of M ; :: thesis: verum
end;
A7: ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier of M
proof
set R = ((Flow M) ~) | the carrier of M;
set S = id the carrier of M;
set T = id ();
A8: id the carrier of M c= id () by ;
A9: ((Flow M) ~) | the carrier of M misses id () by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = ((((Flow M) ~) | the carrier of M) \ (id ())) \/ ((id the carrier of M) \ (id ())) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id ())) \/ {} by
.= ((Flow M) ~) | the carrier of M by ;
hence ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier of M ; :: thesis: verum
end;
A10: (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier of M
proof
set R = (Flow M) | the carrier of M;
set S = id the carrier of M;
set T = id ();
A11: id the carrier of M c= id () by ;
A12: (Flow M) | the carrier of M misses id () by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = (((Flow M) | the carrier of M) \ (id ())) \/ ((id the carrier of M) \ (id ())) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id ())) \/ {} by
.= (Flow M) | the carrier of M by ;
hence (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier of M ; :: thesis: verum
end;
A13: ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier of M
proof
set R = ((Flow M) ~) | the carrier of M;
set S = id the carrier' of M;
set T = id ();
A14: id the carrier' of M c= id () by ;
A15: ((Flow M) ~) | the carrier of M misses id () by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = ((((Flow M) ~) | the carrier of M) \ (id ())) \/ ((id the carrier' of M) \ (id ())) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id ())) \/ {} by
.= ((Flow M) ~) | the carrier of M by ;
hence ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier of M ; :: thesis: verum
end;
A16: (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier of M
proof
set R = (Flow M) | the carrier of M;
set S = id the carrier' of M;
set T = id ();
A17: id the carrier' of M c= id () by ;
A18: (Flow M) | the carrier of M misses id () by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = (((Flow M) | the carrier of M) \ (id ())) \/ ((id the carrier' of M) \ (id ())) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id ())) \/ {} by
.= (Flow M) | the carrier of M by ;
hence (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier of M ; :: thesis: verum
end;
A19: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M
proof
set R = ((Flow M) ~) | the carrier' of M;
set S = id the carrier' of M;
set T = id ();
A20: id the carrier' of M c= id () by ;
A21: ((Flow M) ~) | the carrier' of M misses id () by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = ((((Flow M) ~) | the carrier' of M) \ (id ())) \/ ((id the carrier' of M) \ (id ())) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id ())) \/ {} by
.= ((Flow M) ~) | the carrier' of M by ;
hence ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M ; :: thesis: verum
end;
(((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier' of M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier' of M;
set T = id ();
A22: id the carrier' of M c= id () by ;
A23: (Flow M) | the carrier' of M misses id () by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = (((Flow M) | the carrier' of M) \ (id ())) \/ ((id the carrier' of M) \ (id ())) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id ())) \/ {} by
.= (Flow M) | the carrier' of M by ;
hence (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier' of M ; :: thesis: verum
end;
hence ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id ()) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id ()) = (Flow M) | the carrier' of M ) by A1, A4, A7, A10, A13, A16, A19; :: thesis: verum