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