let x be object ; :: thesis: for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds
card (Im (FSG,x)) > 2
let FSG be Friendship_Graph; :: thesis: ( FSG is without_universal_friend & x in field FSG implies card (Im (FSG,x)) > 2 )
assume A1: FSG is without_universal_friend ; :: thesis: ( not x in field FSG or card (Im (FSG,x)) > 2 )
set I = Im (FSG,x);
assume A2: x in field FSG ; :: thesis: card (Im (FSG,x)) > 2
assume A3: card (Im (FSG,x)) <= 2 ; :: thesis: contradiction
reconsider xx = x as Element of field FSG by A2;
not not card (Im (FSG,x)) = 0 & ... & not card (Im (FSG,x)) = 2 by A3;

per cases then ( card (Im (FSG,x)) = 0 or card (Im (FSG,x)) = 1 or card (Im (FSG,x)) = 2 ) ;

suppose A4: card (Im (FSG,x)) = 0 ; :: thesis: contradiction

xx is universal_friend

proof

let y be object ; :: according to FRIENDS1:def 1 :: thesis: ( y in (field FSG) \ {xx} implies [xx,y] in FSG )
assume A5: y in (field FSG) \ {xx} ; :: thesis: [xx,y] in FSG
then xx <> y by ZFMISC_1:56;
then consider z being object such that
A6: (Im (FSG,x)) /\ (Coim (FSG,y)) = {z} by A5, Def3;
z in {z} by TARSKI:def 1;
then z in Im (FSG,x) by A6, XBOOLE_0:def 4;
hence [xx,y] in FSG by A4; :: thesis: verum

end;

hence contradiction by A1; :: thesis: verum

end;

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

hence contradiction by Th8, INT_2:13; :: thesis: verum

end;

suppose A7: card (Im (FSG,x)) = 2 ; :: thesis: contradiction

then consider y1, y2 being object such that
A8: y1 <> y2 and
A9: Im (FSG,x) = {y1,y2} by CARD_2:60;
consider z1 being object such that
A10: z1 in (field FSG) \ {x} and
A11: not [xx,z1] in FSG by A1, Def1;
A12: z1 <> x by A10, ZFMISC_1:56;
then consider p being object such that
A13: (Im (FSG,x)) /\ (Coim (FSG,z1)) = {p} by A10, A2, Def3;
A14: for y1, y2 being object st y1 <> y2 & Im (FSG,x) = {y1,y2} holds
(Im (FSG,x)) /\ (Im (FSG,z1)) <> {y1}

proof

let y1, y2 be object ; :: thesis: ( y1 <> y2 & Im (FSG,x) = {y1,y2} implies (Im (FSG,x)) /\ (Im (FSG,z1)) <> {y1} )
assume that
A15: y1 <> y2 and
A16: Im (FSG,x) = {y1,y2} ; :: thesis: (Im (FSG,x)) /\ (Im (FSG,z1)) <> {y1}
A17: y1 in {y1} by TARSKI:def 1;
assume A18: (Im (FSG,x)) /\ (Im (FSG,z1)) = {y1} ; :: thesis: contradiction
then y1 in Im (FSG,z1) by A17, XBOOLE_0:def 4;
then A19: [z1,y1] in FSG by RELAT_1:169;
then ( y1 in field FSG & z1 <> y1 ) by RELAT_1:15, Lm2;
then consider t being object such that
A20: (Im (FSG,y1)) /\ (Coim (FSG,z1)) = {t} by Def3, A10;
A21: t in {t} by TARSKI:def 1;
then t in Im (FSG,y1) by A20, XBOOLE_0:def 4;
then A22: [y1,t] in FSG by RELAT_1:169;
then A23: y1 <> t by Lm2;
A24: y1 in Im (FSG,x) by A16, TARSKI:def 2;
then A25: [x,y1] in FSG by RELAT_1:169;
then A26: ( x <> y1 & y1 in field FSG ) by Lm2, RELAT_1:15;
then consider x1x being object such that
A27: (Im (FSG,x)) /\ (Coim (FSG,y1)) = {x1x} by A2, Def3;
A28: x1x in {x1x} by TARSKI:def 1;
then A29: x1x in Im (FSG,x) by A27, XBOOLE_0:def 4;
Coim (FSG,y1) = Im (FSG,y1) by Th2;
then x1x in Im (FSG,y1) by A28, A27, XBOOLE_0:def 4;
then A30: [y1,x1x] in FSG by RELAT_1:169;
then y1 <> x1x by Lm2;
then A31: [y1,y2] in FSG by A29, A16, TARSKI:def 2, A30;
y2 in Im (FSG,x) by A16, TARSKI:def 2;
then A32: [xx,y2] in FSG by RELAT_1:169;
consider z2 being object such that
A33: z2 in (field FSG) \ {y1} and
A34: not [y1,z2] in FSG by A26, A1, Def1;
A35: Coim (FSG,z2) = Im (FSG,z2) by Th2;
z1 <> z2 by A19, Lm3, A34;
then consider w being object such that
A36: (Im (FSG,z2)) /\ (Coim (FSG,z1)) = {w} by A10, A33, Def3;
A37: Coim (FSG,z1) = Im (FSG,z1) by Th2;
then A38: t in Im (FSG,z1) by A21, A20, XBOOLE_0:def 4;
A39: w in {w} by TARSKI:def 1;
then A40: w in Im (FSG,z1) by A36, A37, XBOOLE_0:def 4;
w in Im (FSG,z2) by A39, A36, XBOOLE_0:def 4;
then A41: [z2,w] in FSG by RELAT_1:169;
A42: [z1,w] in FSG by A40, RELAT_1:169;
A43: t <> w

proof

x <> z2 by A34, A25, Lm3;
then consider s being object such that
A44: (Im (FSG,x)) /\ (Coim (FSG,z2)) = {s} by A2, A33, Def3;
A45: s in {s} by TARSKI:def 1;
then s in Im (FSG,z2) by A35, A44, XBOOLE_0:def 4;
then [z2,s] in FSG by RELAT_1:169;
then A46: [s,z2] in FSG by Lm3;
assume A47: t = w ; :: thesis: contradiction
A48: ( [x,y1] in FSG & [y1,z1] in FSG ) by A24, RELAT_1:169, A19, Lm3;
A49: ( y1 <> z2 & [w,z2] in FSG ) by A33, ZFMISC_1:56, A41, Lm3;
s in Im (FSG,x) by A45, A44, XBOOLE_0:def 4;
then [y2,z2] in FSG by A46, A34, A16, TARSKI:def 2;
then y2 = t by A49, A47, A31, A22, Lm5;
then [y2,z1] in FSG by A42, Lm3, A47;
hence contradiction by A48, A32, Lm5, A12, A15; :: thesis: verum

end;

y1 <> w by A41, Lm3, A34;
then A50: card {y1,t,w} = 3 by A43, CARD_2:58, A23;
A51: y1 in Im (FSG,z1) by A17, A18, XBOOLE_0:def 4;
card (Im (FSG,z1)) = 2 by A11, A10, Th9, A7;
hence contradiction by ZFMISC_1:133, A38, A40, A51, NAT_1:43, A50; :: thesis: verum

end;

Coim (FSG,z1) = Im (FSG,z1) by Th2;
then A52: ( p <> y1 & p <> y2 ) by A14, A13, A8, A9;
p in {p} by TARSKI:def 1;
then p in Im (FSG,x) by XBOOLE_0:def 4, A13;
hence contradiction by A52, A9, TARSKI:def 2; :: thesis: verum

end;

end;