let X, Y be set ; :: thesis: ( X c= Y implies CompleteSGraph X c= CompleteSGraph Y )
assume A1: X c= Y ; :: thesis: CompleteSGraph X c= CompleteSGraph Y
let a be object ; :: 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
A2: a = V and
A3: card V <= 2 ;
V is Subset of Y by A1, XBOOLE_1:1;
hence a in CompleteSGraph Y by A2, A3; :: thesis: verum