let it1, it2 be Nat; ( ex C being finite Clique of G st order C = it1 & ( for T being finite Clique of G holds order T <= it1 ) & ex C being finite Clique of G st order C = it2 & ( for T being finite Clique of G holds order T <= it2 ) implies it1 = it2 )
assume that
A1:
ex C being finite Clique of G st order C = it1
and
B1:
for T being finite Clique of G holds order T <= it1
and
A2:
ex C being finite Clique of G st order C = it2
and
B2:
for T being finite Clique of G holds order T <= it2
; it1 = it2
consider C1 being finite Clique of G such that
C1:
order C1 = it1
by A1;
consider C2 being finite Clique of G such that
D1:
order C2 = it2
by A2;
( it1 <= it2 & it2 <= it1 )
by B1, B2, C1, D1;
hence
it1 = it2
by XXREAL_0:1; verum