let x, y be object ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

per cases ( not [x,y] in FSG or [x,y] in FSG ) ;

suppose not [x,y] in FSG ; :: thesis: card (Im (FSG,x)) = card (Im (FSG,y))

hence card (Im (FSG,x)) = card (Im (FSG,y)) by A2, A3, Th9; :: thesis: verum

end;

suppose A4: [x,y] in FSG ; :: thesis: 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 ; :: thesis: contradiction
then y = w by A20, A4, Lm5, A18;
hence contradiction by A17, TARSKI:def 2; :: thesis: verum

end;

A21: y <> z by A12, Lm2;
not [y,w] in FSG

proof

assume A22: [y,w] in FSG ; :: thesis: contradiction
[x,z] in FSG by A8, RELAT_1:169;
then x = w by A22, A15, A4, Lm5, A21;
hence contradiction by A17, TARSKI:def 2; :: thesis: verum

end;

hence card (Im (FSG,y)) = card (Im (FSG,w)) by A3, A16, Th9
.= card (Im (FSG,x)) by A2, Th9, A19, A16 ;
:: thesis: verum

end;

end;