let x, y, z be object ; :: thesis: for P being finite Relation
for t being object st P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P holds
z = t
let P be finite Relation; :: thesis: for t being object st P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P holds
z = t
let t be object ; :: thesis: ( P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P implies z = t )
assume that
A1: ( P is friendship_graph_like & x <> y ) and
A2: [x,z] in P and
A3: [z,y] in P and
A4: [x,t] in P and
A5: [t,y] in P ; :: thesis: z = t
( x in field P & y in field P ) by A2, RELAT_1:15, A3;
then consider d being object such that
A6: (Im (P,x)) /\ (Coim (P,y)) = {d} by A1;
A7: y in {y} by TARSKI:def 1;
then A8: t in Coim (P,y) by RELAT_1:def 14, A5;
A9: z in Coim (P,y) by A7, RELAT_1:def 14, A3;
z in Im (P,x) by A2, RELAT_1:169;
then z in {d} by A9, A6, XBOOLE_0:def 4;
then A10: z = d by TARSKI:def 1;
t in Im (P,x) by A4, RELAT_1:169;
then t in {d} by A8, A6, XBOOLE_0:def 4;
hence z = t by A10, TARSKI:def 1; :: thesis: verum