let x, y be object ; for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG & y in field FSG holds
card (Im (FSG,x)) = card (Im (FSG,y))
let FSG be Friendship_Graph; ( FSG is without_universal_friend & x in field FSG & y in field FSG implies card (Im (FSG,x)) = card (Im (FSG,y)) )
assume that
A1:
FSG is without_universal_friend
and
A2:
x in field FSG
and
A3:
y in field FSG
; card (Im (FSG,x)) = card (Im (FSG,y))
per cases
( not [x,y] in FSG or [x,y] in FSG )
;
suppose A4:
[x,y] in FSG
;
card (Im (FSG,x)) = card (Im (FSG,y))then
x <> y
by Lm2;
then A5:
card {x,y} = 2
by CARD_2:57;
x <> y
by A4, Lm2;
then consider z being
object such that A6:
(Im (FSG,x)) /\ (Coim (FSG,y)) = {z}
by A2, A3, Def3;
A7:
z in {z}
by TARSKI:def 1;
then A8:
z in Im (
FSG,
x)
by A6, XBOOLE_0:def 4;
then A9:
[x,z] in FSG
by RELAT_1:169;
then A10:
z in field FSG
by RELAT_1:15;
Coim (
FSG,
y)
= Im (
FSG,
y)
by Th2;
then A11:
z in Im (
FSG,
y)
by A7, A6, XBOOLE_0:def 4;
then A12:
[y,z] in FSG
by RELAT_1:169;
then
[z,y] in FSG
by Lm3;
then A13:
y in Im (
FSG,
z)
by RELAT_1:169;
[z,x] in FSG
by A9, Lm3;
then
x in Im (
FSG,
z)
by RELAT_1:169;
then
card ((Im (FSG,z)) \ {x,y}) = (card (Im (FSG,z))) - (card {x,y})
by A13, ZFMISC_1:32, CARD_2:44;
then
card ((Im (FSG,z)) \ {x,y}) > 2
- 2
by A5, A10, A1, Th10, XREAL_1:9;
then
card ((Im (FSG,z)) \ {x,y}) > 0
;
then
not
(Im (FSG,z)) \ {x,y} is
empty
;
then consider w being
object such that A14:
w in (Im (FSG,z)) \ {x,y}
;
A15:
[z,w] in FSG
by A14, RELAT_1:169;
then A16:
w in field FSG
by RELAT_1:15;
A17:
not
w in {x,y}
by A14, XBOOLE_0:def 5;
A18:
x <> z
by A9, Lm2;
A19:
not
[x,w] in FSG
proof
A20:
(
[w,z] in FSG &
[y,z] in FSG )
by A15, Lm3, A11, RELAT_1:169;
assume
[x,w] in FSG
;
contradiction
then
y = w
by A20, A4, Lm5, A18;
hence
contradiction
by A17, TARSKI:def 2;
verum
end; A21:
y <> z
by A12, Lm2;
not
[y,w] in FSG
hence card (Im (FSG,y)) =
card (Im (FSG,w))
by A3, A16, Th9
.=
card (Im (FSG,x))
by A2, Th9, A19, A16
;
verum end; end;