let FSG be Friendship_Graph; :: thesis: for x, y being Element of field FSG st x is universal_friend & x <> y holds
ex z being object st
( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )
set F = field FSG;
let x, y be Element of field FSG; :: thesis: ( x is universal_friend & x <> y implies ex z being object st
( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} ) )
assume that
A1: x is universal_friend and
A2: x <> y ; :: thesis: ex z being object st
( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )
A3: not field FSG is empty

proof

assume field FSG is empty ; :: thesis: contradiction
then ( x = {} & y = {} ) by SUBSET_1:def 1;
hence contradiction by A2; :: thesis: verum

end;

then A4: y in (field FSG) \ {x} by A2, ZFMISC_1:56;
consider z being object such that
A5: {z} = (Im (FSG,x)) /\ (Coim (FSG,y)) by A2, A3, Def3;
A6: z in {z} by TARSKI:def 1;
then z in Im (FSG,x) by A5, XBOOLE_0:def 4;
then A7: [x,z] in FSG by RELAT_1:169;
then A8: [z,x] in FSG by Lm3;
then A9: x in Im (FSG,z) by RELAT_1:169;
Coim (FSG,y) = Im (FSG,y) by Th2;
then A10: z in Im (FSG,y) by A6, A5, XBOOLE_0:def 4;
then A11: [y,z] in FSG by RELAT_1:169;
A12: Im (FSG,y) c= {x,z}

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in Im (FSG,y) or d in {x,z} )
assume d in Im (FSG,y) ; :: thesis: d in {x,z}
then A13: [y,d] in FSG by RELAT_1:169;
assume A14: not d in {x,z} ; :: thesis: contradiction
then A15: d <> x by TARSKI:def 2;
d in field FSG by A13, RELAT_1:15;
then d in (field FSG) \ {x} by A15, ZFMISC_1:56;
then [x,d] in FSG by A1;
then A16: [d,x] in FSG by Lm3;
d <> z by A14, TARSKI:def 2;
hence contradiction by A16, A2, A13, Lm5, A11, A8; :: thesis: verum

end;

take z ; :: thesis: ( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )
[x,y] in FSG by A1, A4;
then A17: [y,x] in FSG by Lm3;
then x in Im (FSG,y) by RELAT_1:169;
then {x,z} c= Im (FSG,y) by A10, ZFMISC_1:32;
hence Im (FSG,y) = {x,z} by A12; :: thesis: Im (FSG,z) = {x,y}
A18: [z,y] in FSG by A11, Lm3;
A19: Im (FSG,z) c= {x,y}

proof

let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in Im (FSG,z) or d in {x,y} )
assume d in Im (FSG,z) ; :: thesis: d in {x,y}
then A20: [z,d] in FSG by RELAT_1:169;
assume A21: not d in {x,y} ; :: thesis: contradiction
then A22: d <> x by TARSKI:def 2;
d in field FSG by A20, RELAT_1:15;
then d in (field FSG) \ {x} by A22, ZFMISC_1:56;
then [x,d] in FSG by A1;
then A23: [d,x] in FSG by Lm3;
A24: x <> z by A7, Lm2;
d <> y by A21, TARSKI:def 2;
hence contradiction by A23, A24, A20, Lm5, A17, A18; :: thesis: verum

end;

y in Im (FSG,z) by A18, RELAT_1:169;
then {x,y} c= Im (FSG,z) by A9, ZFMISC_1:32;
hence Im (FSG,z) = {x,y} by A19; :: thesis: verum