let x, y be object ; :: thesis: for FSG being Friendship_Graph st x in field FSG & y in field FSG & not [x,y] in FSG holds
card (Im (FSG,x)) = card (Im (FSG,y))
let FSG be Friendship_Graph; :: thesis: ( x in field FSG & y in field FSG & not [x,y] in FSG implies card (Im (FSG,x)) = card (Im (FSG,y)) )
set cx = card (Im (FSG,x));
set cy = card (Im (FSG,y));
A1: for x, y being object st x in field FSG & y in field FSG & x <> y & not [x,y] in FSG holds
(card (Im (FSG,x))) - 1 <= card (Im (FSG,y))

proof

let x, y be object ; :: thesis: ( x in field FSG & y in field FSG & x <> y & not [x,y] in FSG implies (card (Im (FSG,x))) - 1 <= card (Im (FSG,y)) )
assume that
A2: x in field FSG and
A3: y in field FSG and
A4: x <> y and
A5: not [x,y] in FSG ; :: thesis: (card (Im (FSG,x))) - 1 <= card (Im (FSG,y))
consider z being object such that
A6: (Im (FSG,x)) /\ (Coim (FSG,y)) = {z} by A2, A3, A4, Def3;
defpred S₁[ object , object ] means ( [$1,$2] in FSG & [$2,y] in FSG );
set Ix = Im (FSG,x);
set Iy = Im (FSG,y);
A7: for r being object st r in (Im (FSG,x)) \ {z} holds
ex t being object st S₁[r,t]

proof

let r be object ; :: thesis: ( r in (Im (FSG,x)) \ {z} implies ex t being object st S₁[r,t] )
assume r in (Im (FSG,x)) \ {z} ; :: thesis: ex t being object st S₁[r,t]
then A8: [x,r] in FSG by RELAT_1:169;
then r in field FSG by RELAT_1:15;
then consider t being object such that
A9: (Im (FSG,r)) /\ (Coim (FSG,y)) = {t} by A8, A5, A3, Def3;
take t ; :: thesis: S₁[r,t]
A10: t in {t} by TARSKI:def 1;
Coim (FSG,y) = Im (FSG,y) by Th2;
then t in Im (FSG,y) by A10, A9, XBOOLE_0:def 4;
then A11: [y,t] in FSG by RELAT_1:169;
t in Im (FSG,r) by A10, A9, XBOOLE_0:def 4;
hence S₁[r,t] by RELAT_1:169, A11, Lm3; :: thesis: verum

end;

consider h being Function such that
A12: ( dom h = (Im (FSG,x)) \ {z} & ( for w being object st w in (Im (FSG,x)) \ {z} holds
S₁[w,h . w] ) ) from CLASSES1:sch 1(A7);
A13: rng h c= Im (FSG,y)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng h or t in Im (FSG,y) )
assume t in rng h ; :: thesis: t in Im (FSG,y)
then ex r being object st
( r in dom h & h . r = t ) by FUNCT_1:def 3;
then [t,y] in FSG by A12;
then [y,t] in FSG by Lm3;
hence t in Im (FSG,y) by RELAT_1:169; :: thesis: verum

end;

z in {z} by TARSKI:def 1;
then A14: z in Im (FSG,x) by A6, XBOOLE_0:def 4;
not z in (Im (FSG,x)) \ {z} by ZFMISC_1:56;
then A15: 1 + (card ((Im (FSG,x)) \ {z})) = card (((Im (FSG,x)) \ {z}) \/ {z}) by CARD_2:41
.= card (Im (FSG,x)) by ZFMISC_1:116, A14 ;
for x1, x2 being object st x1 in dom h & x2 in dom h & h . x1 = h . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )
assume that
A16: x1 in dom h and
A17: x2 in dom h and
A18: h . x1 = h . x2 ; :: thesis: x1 = x2
A19: ( [x1,(h . x1)] in FSG & [x2,(h . x1)] in FSG ) by A12, A16, A17, A18;
A20: ( h . x1 <> x & [x,x1] in FSG ) by A12, A16, A5, RELAT_1:169;
[x,x2] in FSG by A12, A17, RELAT_1:169;
hence x1 = x2 by A20, Lm5, A19; :: thesis: verum

end;

then Segm (card ((Im (FSG,x)) \ {z})) c= Segm (card (Im (FSG,y))) by A13, FUNCT_1:def 4, A12, CARD_1:10;
hence (card (Im (FSG,x))) - 1 <= card (Im (FSG,y)) by A15, NAT_1:39; :: thesis: verum

end;

assume that
A21: ( x in field FSG & y in field FSG ) and
A22: not [x,y] in FSG ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))
A23: not [y,x] in FSG by A22, Lm3;

per cases ( x = y or card (Im (FSG,x)) = card (Im (FSG,y)) or ( x <> y & card (Im (FSG,x)) <> card (Im (FSG,y)) ) ) ;

suppose ( x = y or card (Im (FSG,x)) = card (Im (FSG,y)) ) ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

hence card (Im (FSG,x)) = card (Im (FSG,y)) ; :: thesis: verum

end;

suppose A24: ( x <> y & card (Im (FSG,x)) <> card (Im (FSG,y)) ) ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

A25: ((card (Im (FSG,x))) + 1) - 1 = card (Im (FSG,x)) ;
(card (Im (FSG,y))) - 1 <= card (Im (FSG,x)) by A24, A1, A21, A23;
then A26: card (Im (FSG,y)) <= (card (Im (FSG,x))) + 1 by A25, XREAL_1:9;
A27: not 2 divides 1 by INT_2:13;
A28: ((card (Im (FSG,y))) + 1) - 1 = card (Im (FSG,y)) ;
(card (Im (FSG,x))) - 1 <= card (Im (FSG,y)) by A24, A1, A21, A22;
then A29: card (Im (FSG,x)) <= (card (Im (FSG,y))) + 1 by A28, XREAL_1:9;
A30: ( 2 divides card (Im (FSG,x)) & 2 divides card (Im (FSG,y)) ) by Th8;

per cases ( card (Im (FSG,y)) < (card (Im (FSG,x))) + 1 or card (Im (FSG,y)) = (card (Im (FSG,x))) + 1 ) by XXREAL_0:1, A26;

suppose card (Im (FSG,y)) < (card (Im (FSG,x))) + 1 ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

then card (Im (FSG,y)) <= card (Im (FSG,x)) by NAT_1:13;
then card (Im (FSG,y)) < card (Im (FSG,x)) by A24, XXREAL_0:1;
then (card (Im (FSG,y))) + 1 <= card (Im (FSG,x)) by NAT_1:13;
then (card (Im (FSG,y))) + 1 = card (Im (FSG,x)) by A29, XXREAL_0:1;
hence card (Im (FSG,x)) = card (Im (FSG,y)) by A27, A30, INT_2:1; :: thesis: verum

end;

suppose card (Im (FSG,y)) = (card (Im (FSG,x))) + 1 ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

hence card (Im (FSG,x)) = card (Im (FSG,y)) by A30, A27, INT_2:1; :: thesis: verum

end;

end;

end;

end;