let G be with_finite_clique# SimpleGraph; :: thesis: ( 2 <= clique# G implies for D being finite Clique of (Mycielskian G) holds order D <= clique# G )
assume A: 2 <= clique# G ; :: thesis: for D being finite Clique of (Mycielskian G) holds order D <= clique# G
let D be finite Clique of (Mycielskian G); :: thesis: order D <= clique# G
assume Ba: order D > clique# G ; :: thesis: contradiction
set MG = Mycielskian G;
set uG = union G;
Da1: Vertices D c= Vertices (Mycielskian G) by ZFMISC_1:77;
Da2: Edges D c= Edges (Mycielskian G) by SG6e;
2 < order D by Ba, A, XXREAL_0:2;
then Fz: 2 + 1 <= order D by NAT_1:13;

per cases ( D c= G or not D c= G ) ;

suppose D c= G ; :: thesis: contradiction

hence contradiction by Ba, Lcliqueno; :: thesis: verum

end;

suppose not D c= G ; :: thesis: contradiction

then consider e being set such that
B2: e in D and
C2: not e in G by TARSKI:def 3;

now :: thesis: not Vertices D c= Vertices G

assume A3: Vertices D c= Vertices G ; :: thesis: contradiction
B3za: e <> {} by C2, SG1;

now :: thesis: e in Edges D

assume not e in Edges D ; :: thesis: contradiction
then consider y being set such that
A4: e = {y} and
B4: y in Vertices D by B3za, B2, SG2;
thus contradiction by C2, A4, B4, A3, Vertices0; :: thesis: verum

end;

then consider x, y being set such that
x <> y and
D3a: x in Vertices D and
D3b: y in Vertices D and
D3: e = {x,y} by SG4;
thus contradiction by B2, A3, D3, C2, M1, D3a, D3b; :: thesis: verum

end;

then consider v being set such that
A1: v in Vertices D and
B1: not v in Vertices G by TARSKI:def 3;
3 c= order D by Fz, NAT_1:39;
then consider v1, v2 being set such that
C1a: v1 in Vertices D and
C1b: v2 in Vertices D and
C1c: v1 <> v and
C1d: v2 <> v and
C1e: v1 <> v2 by card3;
{v,v1} in D by A1, C1a, Clique2a;
then E1a: {v,v1} in Edges D by C1c, SG4a;
{v,v2} in D by A1, C1b, Clique2a;
then E1b: {v,v2} in Edges D by C1d, SG4a;
{v1,v2} in D by C1a, C1b, Clique2a;
then E1c: {v1,v2} in Edges D by C1e, SG4a;

per cases ( v = union G or ex x being set st
( x in union G & v = [x,(union G)] ) ) by A1, Da1, B1, M0v1;

suppose S2: v = union G ; :: thesis: contradiction

consider x being set such that
x in union G and
F1a: v1 = [x,(union G)] by S2, E1a, Da2, M0e2;
consider y being set such that
y in union G and
F1b: v2 = [y,(union G)] by S2, E1b, Da2, M0e2;
thus contradiction by E1c, Da2, F1a, F1b, M0e3; :: thesis: verum

end;

suppose ex x being set st
( x in union G & v = [x,(union G)] ) ; :: thesis: contradiction

then consider x being set such that
S2a: x in union G and
S2b: v = [x,(union G)] ;
set E = D SubgraphInducedBy (union G);
reconsider F = G SubgraphInducedBy ({x} \/ (union (D SubgraphInducedBy (union G)))) as finite SimpleGraph ;
Z2b: Vertices F = {x} \/ (Vertices (D SubgraphInducedBy (union G)))

proof

thus Vertices F c= {x} \/ (Vertices (D SubgraphInducedBy (union G))) :: according to XBOOLE_0:def 10 :: thesis: {x} \/ (Vertices (D SubgraphInducedBy (union G))) c= Vertices F

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Vertices F or a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) )
assume a in Vertices F ; :: thesis: a in {x} \/ (Vertices (D SubgraphInducedBy (union G)))
then a in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by Sub5;
then C5: a in {x} \/ (union (D SubgraphInducedBy (union G))) by XBOOLE_0:def 4;

per cases ( a in {x} or a in union (D SubgraphInducedBy (union G)) ) by C5, XBOOLE_0:def 3;

suppose a in {x} ; :: thesis: a in {x} \/ (Vertices (D SubgraphInducedBy (union G)))

hence a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose a in union (D SubgraphInducedBy (union G)) ; :: thesis: a in {x} \/ (Vertices (D SubgraphInducedBy (union G)))

hence a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) or a in Vertices F )
assume A3: a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) ; :: thesis: a in Vertices F

per cases ( a in {x} or a in Vertices (D SubgraphInducedBy (union G)) ) by A3, XBOOLE_0:def 3;

suppose a in {x} ; :: thesis: a in Vertices F

then A4: a = x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
then x in {x} \/ (union (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3;
then x in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by S2a, XBOOLE_0:def 4;
hence a in Vertices F by A4, Sub5; :: thesis: verum

end;

suppose a in Vertices (D SubgraphInducedBy (union G)) ; :: thesis: a in Vertices F

then a in (union D) /\ (union G) by Sub5;
then a in union G by XBOOLE_0:def 4;
then a in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by A3, XBOOLE_0:def 4;
hence a in Vertices F by Sub5; :: thesis: verum

end;

end;

end;

Z2d: union (D SubgraphInducedBy (union G)) c= union D by ZFMISC_1:77;

Z2c: now :: thesis: not x in union (D SubgraphInducedBy (union G))

assume x in union (D SubgraphInducedBy (union G)) ; :: thesis: contradiction
then {[x,(union G)],x} in D by Z2d, A1, S2b, Clique2a;
hence contradiction by M0e4a; :: thesis: verum

end;

reconsider Fs = F as SimpleGraph-like Subset of G ;

now :: thesis: for a, b being set st a <> b & a in union Fs & b in union Fs holds
{a,b} in Edges Fs

let a, b be set ; :: thesis: ( a <> b & a in union Fs & b in union Fs implies {a,b} in Edges Fs )
assume that
A4: a <> b and
B4: a in union Fs and
C4: b in union Fs ; :: thesis: {a,b} in Edges Fs
D4ba: a in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by B4, Sub5;
then D4b: ( a in union G & a in {x} \/ (union (D SubgraphInducedBy (union G))) ) by XBOOLE_0:def 4;
E4ba: b in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by C4, Sub5;
then E4b: ( b in union G & b in {x} \/ (union (D SubgraphInducedBy (union G))) ) by XBOOLE_0:def 4;
F4a: a in Vertices G by D4ba, XBOOLE_0:def 4;
F4b: b in Vertices G by E4ba, XBOOLE_0:def 4;
x in {x} by TARSKI:def 1;
then H4: x in {x} \/ (union (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3;
{a,b} in Fs

proof

per cases ( ( a in {x} & b in {x} ) or ( a in {x} & b in union (D SubgraphInducedBy (union G)) ) or ( b in {x} & a in union (D SubgraphInducedBy (union G)) ) or ( a in union (D SubgraphInducedBy (union G)) & b in union (D SubgraphInducedBy (union G)) ) ) by D4b, E4b, XBOOLE_0:def 3;

suppose ( a in {x} & b in {x} ) ; :: thesis: {a,b} in Fs

then A5: ( a = x & b = x ) by TARSKI:def 1;
then {a,b} = {x} by ENUMSET1:29;
hence {a,b} in Fs by A5, B4, Vertices0; :: thesis: verum

end;

suppose S4: ( a in {x} & b in union (D SubgraphInducedBy (union G)) ) ; :: thesis: {a,b} in Fs

then A5: a = x by TARSKI:def 1;
b in (union D) /\ (union G) by S4, Sub5;
then B5: ( b in union D & b in union G ) by XBOOLE_0:def 4;
then {[x,(union G)],b} in D by A1, S2b, Clique2a;
then {x,b} in G by B5, M0e4b;
hence {a,b} in Fs by H4, A5, E4b, Sub6; :: thesis: verum

end;

suppose S4: ( b in {x} & a in union (D SubgraphInducedBy (union G)) ) ; :: thesis: {a,b} in Fs

then A5: b = x by TARSKI:def 1;
a in (union D) /\ (union G) by S4, Sub5;
then B5: ( a in union D & a in union G ) by XBOOLE_0:def 4;
then {[x,(union G)],a} in D by A1, S2b, Clique2a;
then {x,a} in G by B5, M0e4b;
hence {a,b} in Fs by H4, A5, D4b, Sub6; :: thesis: verum

end;

suppose ( a in union (D SubgraphInducedBy (union G)) & b in union (D SubgraphInducedBy (union G)) ) ; :: thesis: {a,b} in Fs

then ( a in (union D) /\ (union G) & b in (union D) /\ (union G) ) by Sub5;
then ( a in union D & b in union D ) by XBOOLE_0:def 4;
then {a,b} in D by Clique2a;
then {a,b} in G by F4a, F4b, M1;
hence {a,b} in Fs by D4b, E4b, Sub6; :: thesis: verum

end;

end;

end;

hence {a,b} in Edges Fs by A4, SG4a; :: thesis: verum

end;

then Y2a: Fs is clique by Lclique1;
U2: Vertices D c= {v} \/ (Vertices (D SubgraphInducedBy (union G)))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Vertices D or a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) )
assume A3: a in Vertices D ; :: thesis: a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))

per cases ( a = v or a <> v ) ;

suppose a = v ; :: thesis: a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))

then a in {v} by TARSKI:def 1;
hence a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose S3: a <> v ; :: thesis: a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))

{a,[x,(union G)]} in D by S2b, A1, A3, Clique2a;
then {a,[x,(union G)]} in Edges D by S3, S2b, SG4a;
then ( a in union G or a = union G ) by Da2, M0e4;
then a in Vertices (D SubgraphInducedBy (union G)) by Fz, MClique3, A3, Sub3;
hence a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

U2a: Vertices (D SubgraphInducedBy (union G)) c= Vertices D by ZFMISC_1:77;
Z2a1: {v} \/ (Vertices (D SubgraphInducedBy (union G))) c= Vertices D

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) or a in Vertices D )
assume a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) ; :: thesis: a in Vertices D
then ( a in {v} or a in Vertices (D SubgraphInducedBy (union G)) ) by XBOOLE_0:def 3;
hence a in Vertices D by A1, U2a, TARSKI:def 1; :: thesis: verum

end;

Z2d: not v in Vertices (D SubgraphInducedBy (union G)) by S2b, Sub1, Aux1;
order F = 1 + (card (Vertices (D SubgraphInducedBy (union G)))) by Z2b, Z2c, CARD_2:41
.= card ({v} \/ (Vertices (D SubgraphInducedBy (union G)))) by Z2d, CARD_2:41
.= order D by Z2a1, U2, XBOOLE_0:def 10 ;
hence contradiction by Ba, Y2a, Lcliqueno; :: thesis: verum

end;

end;

end;

end;