let G be _Graph; :: thesis: for X1, X2 being set
for y being object st X1 misses X2 holds
G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y})
let X1, X2 be set ; :: thesis: for y being object st X1 misses X2 holds
G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y})
let y be object ; :: thesis: ( X1 misses X2 implies G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y}) )
assume X1 misses X2 ; :: thesis: G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y})
then A1: X1 /\ X2 = {} by XBOOLE_0:def 7;
set E1 = G .edgesBetween (X1,{y});
set E2 = G .edgesBetween (X2,{y});
assume not G .edgesBetween (X1,{y}) misses G .edgesBetween (X2,{y}) ; :: thesis: contradiction
then A2: (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) <> {} by XBOOLE_0:def 7;
set e = the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y}));
A3: the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) in (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) by A2;
then the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) in G .edgesBetween (X1,{y}) by XBOOLE_0:def 4;
then the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) SJoins X1,{y},G by Def30;
then consider x1 being object such that
A4: ( x1 in X1 & the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) Joins x1,y,G ) by Th102;
the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) in G .edgesBetween (X2,{y}) by A3, XBOOLE_0:def 4;
then the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) SJoins X2,{y},G by Def30;
then consider x2 being object such that
A5: ( x2 in X2 & the Element of (G .edgesBetween (X1,{y})) /\ (G .edgesBetween (X2,{y})) Joins x2,y,G ) by Th102;
thus contradiction by A1, A4, A5, XBOOLE_0:def 4; :: thesis: verum