set G = { V where V is finite Subset of X : card V <= 2 } ;
A: { V where V is finite Subset of X : card V <= 2 } is subset-closed

proof

let x, y be set ; :: according to CLASSES1:def 1 :: thesis: ( not x in { V where V is finite Subset of X : card V <= 2 } or not y c= x or y in { V where V is finite Subset of X : card V <= 2 } )
assume that
A1: x in { V where V is finite Subset of X : card V <= 2 } and
B1: y c= x ; :: thesis: y in { V where V is finite Subset of X : card V <= 2 }
consider V being finite Subset of X such that
C1: x = V and
D1: card V <= 2 by A1;
reconsider y1 = y as finite Subset of X by C1, B1, XBOOLE_1:1;
card y1 <= card V by B1, C1, NAT_1:43;
then card y1 <= 2 by D1, XXREAL_0:2;
hence y in { V where V is finite Subset of X : card V <= 2 } ; :: thesis: verum

end;

B: { V where V is finite Subset of X : card V <= 2 } is 1 -at_most_dimensional

proof

let x be set ; :: according to SCMYCIEL:def 4 :: thesis: ( x in { V where V is finite Subset of X : card V <= 2 } implies card x c= 1 + 1 )
assume x in { V where V is finite Subset of X : card V <= 2 } ; :: thesis: card x c= 1 + 1
then consider V being finite Subset of X such that
C1: x = V and
D1: card V <= 2 ;
thus card x c= 1 + 1 by C1, D1, NAT_1:39; :: thesis: verum

end;

Z1: {} c= X by XBOOLE_1:2;
card {} <= 2 ;
then {} in { V where V is finite Subset of X : card V <= 2 } by Z1;
then reconsider G = { V where V is finite Subset of X : card V <= 2 } as SimpleGraph by A, B;
Vertices G = X by CSGLem1;
hence { V where V is finite Subset of X : card V <= 2 } is SimpleGraph of X by LSGofX; :: thesis: verum