let M be Pnet; :: thesis: ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M )
A1: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((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 (Elements M);
A2: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A3: ((Flow M) ~) | the carrier' of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ {} by A2, XBOOLE_1:37
.= ((Flow M) ~) | the carrier' of M by A3, XBOOLE_1:83 ;
hence ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M ; :: thesis: verum
end;
A4: (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (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 (Elements M);
A5: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A6: (Flow M) | the carrier' of M misses id (Elements M) by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ {} by A5, XBOOLE_1:37
.= (Flow M) | the carrier' of M by A6, XBOOLE_1:83 ;
hence (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ; :: thesis: verum
end;
A7: ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((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 (Elements M);
A8: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A9: ((Flow M) ~) | the carrier of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ {} by A8, XBOOLE_1:37
.= ((Flow M) ~) | the carrier of M by A9, XBOOLE_1:83 ;
hence ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M ; :: thesis: verum
end;
A10: (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (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 (Elements M);
A11: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A12: (Flow M) | the carrier of M misses id (Elements M) by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (((Flow M) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id (Elements M))) \/ {} by A11, XBOOLE_1:37
.= (Flow M) | the carrier of M by A12, XBOOLE_1:83 ;
hence (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M ; :: thesis: verum
end;
A13: ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((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 (Elements M);
A14: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A15: ((Flow M) ~) | the carrier of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ {} by A14, XBOOLE_1:37
.= ((Flow M) ~) | the carrier of M by A15, XBOOLE_1:83 ;
hence ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M ; :: thesis: verum
end;
A16: (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (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 (Elements M);
A17: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A18: (Flow M) | the carrier of M misses id (Elements M) by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (((Flow M) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id (Elements M))) \/ {} by A17, XBOOLE_1:37
.= (Flow M) | the carrier of M by A18, XBOOLE_1:83 ;
hence (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M ; :: thesis: verum
end;
A19: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((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 (Elements M);
A20: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A21: ((Flow M) ~) | the carrier' of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ {} by A20, XBOOLE_1:37
.= ((Flow M) ~) | the carrier' of M by A21, XBOOLE_1:83 ;
hence ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M ; :: thesis: verum
end;
(((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (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 (Elements M);
A22: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A23: (Flow M) | the carrier' of M misses id (Elements M) by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ {} by A22, XBOOLE_1:37
.= (Flow M) | the carrier' of M by A23, XBOOLE_1:83 ;
hence (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ; :: thesis: verum
end;
hence ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ) by A1, A4, A7, A10, A13, A16, A19; :: thesis: verum