set G = { V where V is finite Subset of X : card V <= 2 } ;
A1: { 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
A2: x in { V where V is finite Subset of X : card V <= 2 } and
A3: 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
A4: x = V and
A5: card V <= 2 by A2;
reconsider y1 = y as finite Subset of X by A4, A3, XBOOLE_1:1;
card y1 <= card V by A3, A4, NAT_1:43;
then card y1 <= 2 by A5, XXREAL_0:2;
hence y in { V where V is finite Subset of X : card V <= 2 } ; :: thesis: verum
end;
A6: { 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
A7: x = V and
A8: card V <= 2 ;
Segm (card V) c= Segm (1 + 1) by A8, NAT_1:39;
hence card x c= 1 + 1 by A7; :: thesis: verum
end;
A9: {} c= X ;
card {} <= 2 ;
then {} in { V where V is finite Subset of X : card V <= 2 } by A9;
then reconsider G = { V where V is finite Subset of X : card V <= 2 } as SimpleGraph by A1, A6;
Vertices G = X by Lm1;
hence { V where V is finite Subset of X : card V <= 2 } is SimpleGraph of X by Def9; :: thesis: verum