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 A1: 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 A2: order D > clique# G ; :: thesis: contradiction
set MG = Mycielskian G;
set uG = union G;
A3: Vertices D c= Vertices (Mycielskian G) by ZFMISC_1:77;
A4: Edges D c= Edges (Mycielskian G) by Th14;
2 < order D by A2, A1, XXREAL_0:2;
then A5: 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 A2, Def15; :: thesis: verum

end;

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

then consider e being object such that
A6: e in D and
A7: not e in G ;

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

assume A8: Vertices D c= Vertices G ; :: thesis: contradiction
A9: e <> {} by A7, Th20;

now :: thesis: e in Edges D

assume not e in Edges D ; :: thesis: contradiction
then consider y being set such that
A10: e = {y} and
A11: y in Vertices D by A9, A6, Th29;
thus contradiction by A7, A10, A11, A8, Th24; :: thesis: verum

end;

then consider x, y being set such that
x <> y and
A12: x in Vertices D and
A13: y in Vertices D and
A14: e = {x,y} by Th11;
thus contradiction by A6, A8, A14, A7, Th103, A12, A13; :: thesis: verum

end;

then consider v being object such that
A15: v in Vertices D and
A16: not v in Vertices G ;
Segm 3 c= Segm (order D) by A5, NAT_1:39;
then consider v1, v2 being object such that
A17: v1 in Vertices D and
A18: v2 in Vertices D and
A19: v1 <> v and
A20: v2 <> v and
A21: v1 <> v2 by Th5;
{v,v1} in D by A15, A17, Th53;
then A22: {v,v1} in Edges D by A19, Th12;
{v,v2} in D by A15, A18, Th53;
then A23: {v,v2} in Edges D by A20, Th12;
{v1,v2} in D by A17, A18, Th53;
then A24: {v1,v2} in Edges D by A21, Th12;

per cases ( v = union G or ex x being set st
( x in union G & v = [x,(union G)] ) ) by A15, A3, A16, Th85;

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

consider x being object such that
x in union G and
A26: v1 = [x,(union G)] by A25, A22, A4, Th94;
consider y being object such that
y in union G and
A27: v2 = [y,(union G)] by A25, A23, A4, Th94;
thus contradiction by A24, A4, A26, A27, Th97; :: 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
A28: x in union G and
A29: v = [x,(union G)] ;
set E = D SubgraphInducedBy (union G);
reconsider F = G SubgraphInducedBy ({x} \/ (union (D SubgraphInducedBy (union G)))) as finite SimpleGraph ;
A30: 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 object ; :: 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 Th45;
then A31: 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 A31, 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in {x} \/ (Vertices (D SubgraphInducedBy (union G))) or a in Vertices F )
assume A32: 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 A32, XBOOLE_0:def 3;

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

then A33: 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 A28, XBOOLE_0:def 4;
hence a in Vertices F by A33, Th45; :: thesis: verum

end;

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

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

end;

end;

end;

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

A35: 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 A34, A15, A29, Th53;
hence contradiction by Th100; :: 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
A36: a <> b and
A37: a in union Fs and
A38: b in union Fs ; :: thesis: {a,b} in Edges Fs
A39: a in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by A37, Th45;
then A40: ( a in union G & a in {x} \/ (union (D SubgraphInducedBy (union G))) ) by XBOOLE_0:def 4;
A41: b in (union G) /\ ({x} \/ (union (D SubgraphInducedBy (union G)))) by A38, Th45;
then A42: ( b in union G & b in {x} \/ (union (D SubgraphInducedBy (union G))) ) by XBOOLE_0:def 4;
A43: a in Vertices G by A39, XBOOLE_0:def 4;
A44: b in Vertices G by A41, XBOOLE_0:def 4;
x in {x} by TARSKI:def 1;
then A45: 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 A40, A42, XBOOLE_0:def 3;

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

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

end;

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

then A48: a = x by TARSKI:def 1;
b in (union D) /\ (union G) by A47, Th45;
then A49: ( b in union D & b in union G ) by XBOOLE_0:def 4;
then {[x,(union G)],b} in D by A15, A29, Th53;
then {x,b} in G by A49, Th101;
hence {a,b} in Fs by A45, A48, A42, Lm10; :: thesis: verum

end;

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

then A51: b = x by TARSKI:def 1;
a in (union D) /\ (union G) by A50, Th45;
then A52: ( a in union D & a in union G ) by XBOOLE_0:def 4;
then {[x,(union G)],a} in D by A15, A29, Th53;
then {x,a} in G by A52, Th101;
hence {a,b} in Fs by A45, A51, A40, Lm10; :: 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 Th45;
then ( a in union D & b in union D ) by XBOOLE_0:def 4;
then {a,b} in D by Th53;
then {a,b} in G by A43, A44, Th103;
hence {a,b} in Fs by A40, A42, Lm10; :: thesis: verum

end;

end;

end;

hence {a,b} in Edges Fs by A36, Th12; :: thesis: verum

end;

then A53: Fs is clique by Th47;
A54: Vertices D c= {v} \/ (Vertices (D SubgraphInducedBy (union G)))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Vertices D or a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) )
assume A55: 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 A56: a <> v ; :: thesis: a in {v} \/ (Vertices (D SubgraphInducedBy (union G)))

{a,[x,(union G)]} in D by A29, A15, A55, Th53;
then {a,[x,(union G)]} in Edges D by A56, A29, Th12;
then ( a in union G or a = union G ) by A4, Th99;
then a in Vertices (D SubgraphInducedBy (union G)) by A5, Th105, A55, Lm8;
hence a in {v} \/ (Vertices (D SubgraphInducedBy (union G))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

proof

let a be object ; :: 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 A15, A57, TARSKI:def 1; :: thesis: verum

end;

A59: not v in Vertices (D SubgraphInducedBy (union G)) by A29, Lm7, Th1;
order F = 1 + (card (Vertices (D SubgraphInducedBy (union G)))) by A30, A35, CARD_2:41
.= card ({v} \/ (Vertices (D SubgraphInducedBy (union G)))) by A59, CARD_2:41
.= order D by A58, A54, XBOOLE_0:def 10 ;
hence contradiction by A2, A53, Def15; :: thesis: verum

end;

end;

end;

end;