set VG = Vertices G;

per cases ( Vertices G is empty or not Vertices G is empty ) ;

suppose Vertices G is empty ; :: thesis: ex b₁ being a_partition of Vertices G st b₁ is Clique-wise

then reconsider S = {} as a_partition of Vertices G by EQREL_1:45;
take S ; :: thesis: S is Clique-wise
for x being set st x in S holds
G SubgraphInducedBy x is Clique of G ;
hence S is Clique-wise by LCliquewise; :: thesis: verum

end;

suppose not Vertices G is empty ; :: thesis: ex b₁ being a_partition of Vertices G st b₁ is Clique-wise

then reconsider cRp1 = Vertices G as non empty set ;
set S = SmallestPartition (Vertices G);
A3: SmallestPartition (Vertices G) = { {x} where x is Element of cRp1 : verum } by EQREL_1:37;
take SmallestPartition (Vertices G) ; :: thesis: SmallestPartition (Vertices G) is Clique-wise

now :: thesis: for z being set st z in SmallestPartition (Vertices G) holds
G SubgraphInducedBy z is Clique of G

let z be set ; :: thesis: ( z in SmallestPartition (Vertices G) implies G SubgraphInducedBy z is Clique of G )
assume A5: z in SmallestPartition (Vertices G) ; :: thesis: G SubgraphInducedBy z is Clique of G
consider x being Element of cRp1 such that
B2: z = {x} and
verum by A3, A5;
G SubgraphInducedBy z = {{},{x}} by B2, SingleSub;
hence G SubgraphInducedBy z is Clique of G by SingleClique; :: thesis: verum

end;

hence SmallestPartition (Vertices G) is Clique-wise by LCliquewise; :: thesis: verum

end;

end;