set G = CompleteSGraph X;
CompleteSGraph X c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in CompleteSGraph X or x in bool X )
assume x in CompleteSGraph X ; :: thesis: x in bool X
then consider V being finite Subset of X such that
A1: x = V and
card V <= 2 ;
thus x in bool X by A1; :: thesis: verum

end;

hence CompleteSGraph X is finite ; :: thesis: verum