let M be Pnet; :: thesis: ( ((Flow M) ~) | the carrier' of M misses id () & (Flow M) | the carrier' of M misses id () & ((Flow M) ~) | the carrier of M misses id () & (Flow M) | the carrier of M misses id () )
set T = id ();
thus ((Flow M) ~) | the carrier' of M misses id () :: thesis: ( (Flow M) | the carrier' of M misses id () & ((Flow M) ~) | the carrier of M misses id () & (Flow M) | the carrier of M misses id () )
proof
set R = ((Flow M) ~) | the carrier' of M;
for x, y being object holds not [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id ())
proof
let x, y be object ; :: thesis: not [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id ())
assume A1: [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id ()) ; :: thesis: contradiction
then A2: [x,y] in ((Flow M) ~) | the carrier' of M by XBOOLE_0:def 4;
A3: [x,y] in id () by ;
A4: [x,y] in (Flow M) ~ by ;
A5: x in the carrier' of M by ;
[y,x] in Flow M by ;
then x <> y by ;
hence contradiction by A3, RELAT_1:def 10; :: thesis: verum
end;
then (((Flow M) ~) | the carrier' of M) /\ (id ()) = {} by RELAT_1:37;
hence ((Flow M) ~) | the carrier' of M misses id () by XBOOLE_0:def 7; :: thesis: verum
end;
thus (Flow M) | the carrier' of M misses id () :: thesis: ( ((Flow M) ~) | the carrier of M misses id () & (Flow M) | the carrier of M misses id () )
proof
set R = (Flow M) | the carrier' of M;
for x, y being object holds not [x,y] in ((Flow M) | the carrier' of M) /\ (id ())
proof
let x, y be object ; :: thesis: not [x,y] in ((Flow M) | the carrier' of M) /\ (id ())
assume A6: [x,y] in ((Flow M) | the carrier' of M) /\ (id ()) ; :: thesis: contradiction
then A7: [x,y] in (Flow M) | the carrier' of M by XBOOLE_0:def 4;
A8: [x,y] in id () by ;
A9: x in the carrier' of M by ;
[x,y] in Flow M by ;
then x <> y by ;
hence contradiction by A8, RELAT_1:def 10; :: thesis: verum
end;
then ((Flow M) | the carrier' of M) /\ (id ()) = {} by RELAT_1:37;
hence (Flow M) | the carrier' of M misses id () by XBOOLE_0:def 7; :: thesis: verum
end;
thus ((Flow M) ~) | the carrier of M misses id () :: thesis: (Flow M) | the carrier of M misses id ()
proof
set R = ((Flow M) ~) | the carrier of M;
for x, y being object holds not [x,y] in (((Flow M) ~) | the carrier of M) /\ (id ())
proof
let x, y be object ; :: thesis: not [x,y] in (((Flow M) ~) | the carrier of M) /\ (id ())
assume A10: [x,y] in (((Flow M) ~) | the carrier of M) /\ (id ()) ; :: thesis: contradiction
then A11: [x,y] in ((Flow M) ~) | the carrier of M by XBOOLE_0:def 4;
A12: [x,y] in id () by ;
A13: [x,y] in (Flow M) ~ by ;
A14: x in the carrier of M by ;
[y,x] in Flow M by ;
then x <> y by ;
hence contradiction by A12, RELAT_1:def 10; :: thesis: verum
end;
then (((Flow M) ~) | the carrier of M) /\ (id ()) = {} by RELAT_1:37;
hence ((Flow M) ~) | the carrier of M misses id () by XBOOLE_0:def 7; :: thesis: verum
end;
set R = (Flow M) | the carrier of M;
for x, y being object holds not [x,y] in ((Flow M) | the carrier of M) /\ (id ())
proof
let x, y be object ; :: thesis: not [x,y] in ((Flow M) | the carrier of M) /\ (id ())
assume A15: [x,y] in ((Flow M) | the carrier of M) /\ (id ()) ; :: thesis: contradiction
then A16: [x,y] in (Flow M) | the carrier of M by XBOOLE_0:def 4;
A17: [x,y] in id () by ;
A18: x in the carrier of M by ;
[x,y] in Flow M by ;
then x <> y by ;
hence contradiction by A17, RELAT_1:def 10; :: thesis: verum
end;
then ((Flow M) | the carrier of M) /\ (id ()) = {} by RELAT_1:37;
hence (Flow M) | the carrier of M misses id () by XBOOLE_0:def 7; :: thesis: verum