consider C being finite Clique of G such that
A1: for D being finite Clique of G holds order D <= order C by Def14;
take itt = order C; :: thesis: ( ex C being finite Clique of G st order C = itt & ( for T being finite Clique of G holds order T <= itt ) )
thus ex A being finite Clique of G st order A = itt ; :: thesis: for T being finite Clique of G holds order T <= itt
let T be finite Clique of G; :: thesis: order T <= itt
thus order T <= itt by A1; :: thesis: verum