let FSG be Friendship_Graph; 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; ( 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
; ex z being object st
( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )
A3:
not field FSG is empty
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 ;
TARSKI:def 3 ( not d in Im (FSG,y) or d in {x,z} )
assume
d in Im (
FSG,
y)
;
d in {x,z}
then A13:
[y,d] in FSG
by RELAT_1:169;
assume A14:
not
d in {x,z}
;
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;
verum
end;
take
z
; ( 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; 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 ;
TARSKI:def 3 ( not d in Im (FSG,z) or d in {x,y} )
assume
d in Im (
FSG,
z)
;
d in {x,y}
then A20:
[z,d] in FSG
by RELAT_1:169;
assume A21:
not
d in {x,y}
;
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;
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; verum