let X, Y be set ; :: thesis: ( X c= Y implies CompleteSGraph X c= CompleteSGraph Y )
assume A: X c= Y ; :: thesis: CompleteSGraph X c= CompleteSGraph Y
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in CompleteSGraph X or a in CompleteSGraph Y )
assume a in CompleteSGraph X ; :: thesis: a in CompleteSGraph Y
then consider V being finite Subset of X such that
A1: a = V and
B1: card V <= 2 ;
V is Subset of Y by A, XBOOLE_1:1;
hence a in CompleteSGraph Y by A1, B1; :: thesis: verum