set uG = union G;
set C = { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ;
set B = { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;
set M = ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ;
reconsider N = ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } as non empty set ;
B: ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } is subset-closed

proof

let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } or not b c= a or b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } )
assume that
A1: a in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } and
B1: b c= a ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }
C1a: {} in {{}} by TARSKI:def 1;
then C1: {} in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by MYCIELSK:4;

per cases ( a in {{}} or a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or a in Edges G or a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or a in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) by A1, MYCIELSK:4;

suppose a in {{}} ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }

then a = {} by TARSKI:def 1;
hence b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by B1, C1; :: thesis: verum

end;

suppose a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }

then consider x being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A2: a = {x} and
verum ;
thus b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by C1, A2, A1, B1, ZFMISC_1:33; :: thesis: verum

end;

suppose a in Edges G ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }

then consider x, y being set such that
x <> y and
B2: x in Vertices G and
C2: y in Vertices G and
D2: a = {x,y} by SG4;
E2: ( b = {} or b = {x} or b = {y} or b = {x,y} ) by D2, B1, ZFMISC_1:36;
( x in (union G) \/ [:(union G),{(union G)}:] & y in (union G) \/ [:(union G),{(union G)}:] ) by B2, C2, XBOOLE_0:def 3;
then ( x in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} & y in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} ) by XBOOLE_0:def 3;
then ( {x} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } & {y} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) ;
hence b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by E2, C1a, D2, A1, MYCIELSK:4; :: thesis: verum

end;

suppose a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }

then consider x, y being Element of union G such that
A2: a = {x,[y,(union G)]} and
B2: {x,y} in Edges G ;
C2: x in union G by B2, SG5;
E2: ( b = {} or b = {x} or b = {[y,(union G)]} or b = {x,[y,(union G)]} ) by A2, B1, ZFMISC_1:36;
x in (union G) \/ [:(union G),{(union G)}:] by C2, XBOOLE_0:def 3;
then x in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then F2: {x} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
( y in union G & union G in {(union G)} ) by B2, SG5, TARSKI:def 1;
then [y,(union G)] in [:(union G),{(union G)}:] by ZFMISC_1:def 2;
then [y,(union G)] in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
then [y,(union G)] in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then {[y,(union G)]} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
hence b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by A2, A1, E2, C1a, F2, MYCIELSK:4; :: thesis: verum

end;

suppose a in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ; :: thesis: b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G }

then consider x being Element of union G such that
A2: a = {(union G),[x,(union G)]} and
C2: x in Vertices G ;
E2: ( b = {} or b = {(union G)} or b = {[x,(union G)]} or b = {(union G),[x,(union G)]} ) by A2, B1, ZFMISC_1:36;
union G in {(union G)} by TARSKI:def 1;
then union G in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then F2: {(union G)} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
( x in union G & union G in {(union G)} ) by C2, TARSKI:def 1;
then [x,(union G)] in [:(union G),{(union G)}:] by ZFMISC_1:def 2;
then [x,(union G)] in (union G) \/ [:(union G),{(union G)}:] by XBOOLE_0:def 3;
then [x,(union G)] in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then {[x,(union G)]} in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ;
hence b in ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } by A2, A1, E2, C1a, F2, MYCIELSK:4; :: thesis: verum

end;

end;

end;

C: N is 1 -at_most_dimensional

proof

let a be set ; :: according to SCMYCIEL:def 4 :: thesis: ( a in N implies card a c= 1 + 1 )
assume Aa: a in N ; :: thesis: card a c= 1 + 1

per cases ( a in {{}} or a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or a in Edges G or a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or a in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) by Aa, MYCIELSK:4;

suppose a in {{}} ; :: thesis: card a c= 1 + 1

then a = {} by TARSKI:def 1;
hence card a c= 1 + 1 ; :: thesis: verum

end;

suppose a in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis: card a c= 1 + 1

then consider x being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A1: a = {x} and
verum ;
card a = 1 by A1, CARD_1:30;
hence card a c= 1 + 1 by NAT_1:39; :: thesis: verum

end;

suppose a in Edges G ; :: thesis: card a c= 1 + 1

hence card a c= 1 + 1 by Lnatmost; :: thesis: verum

end;

suppose a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: card a c= 1 + 1

then consider x, y being Element of union G such that
A1: a = {x,[y,(union G)]} and
{x,y} in Edges G ;
card {x,[y,(union G)]} <= 2 by CARD_2:50;
hence card a c= 1 + 1 by A1, NAT_1:39; :: thesis: verum

end;

suppose a in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ; :: thesis: card a c= 1 + 1

then consider x being Element of union G such that
A1: a = {(union G),[x,(union G)]} and
x in Vertices G ;
card {(union G),[x,(union G)]} <= 2 by CARD_2:50;
hence card a c= 1 + 1 by A1, NAT_1:39; :: thesis: verum

end;

end;

end;

thus ((({{}} \/ { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ) \/ (Edges G)) \/ { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ) \/ { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } is SimpleGraph by B, C; :: thesis: verum