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 ;
A1: ((({{}} \/ { {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
A2: 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
A3: 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 }
A4: {} in {{}} by TARSKI:def 1;
then A5: {} 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 A2, 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 A3, A5; :: 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
A6: a = {x} ;
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 A5, A6, A2, A3, 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
A7: x in Vertices G and
A8: y in Vertices G and
A9: a = {x,y} by Th11;
A10: ( b = {} or b = {x} or b = {y} or b = {x,y} ) by A9, A3, ZFMISC_1:36;
( x in (union G) \/ [:(union G),{(union G)}:] & y in (union G) \/ [:(union G),{(union G)}:] ) by A7, A8, 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 A10, A4, A9, A2, 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
A11: a = {x,[y,(union G)]} and
A12: {x,y} in Edges G ;
A13: x in union G by A12, Th13;
A14: ( b = {} or b = {x} or b = {[y,(union G)]} or b = {x,[y,(union G)]} ) by A11, A3, ZFMISC_1:36;
x in (union G) \/ [:(union G),{(union G)}:] by A13, XBOOLE_0:def 3;
then x in ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} by XBOOLE_0:def 3;
then A15: {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 A12, Th13, 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 A11, A2, A14, A4, A15, 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
A16: a = {(union G),[x,(union G)]} and
A17: x in Vertices G ;
A18: ( b = {} or b = {(union G)} or b = {[x,(union G)]} or b = {(union G),[x,(union G)]} ) by A16, A3, 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 A19: {(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 A17, 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 A16, A2, A18, A4, A19, MYCIELSK:4; :: thesis: verum

end;

end;

end;

A20: 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 A21: 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 A21, 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
A22: a = {x} ;
A23: card a = 1 by A22, CARD_1:30;
Segm 1 c= Segm (1 + 1) by NAT_1:39;
hence card a c= 1 + 1 by A23; :: thesis: verum

end;

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

hence card a c= 1 + 1 by Def4; :: 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
A24: a = {x,[y,(union G)]} and
{x,y} in Edges G ;
card {x,[y,(union G)]} <= 2 by CARD_2:50;
then Segm (card {x,[y,(union G)]}) c= Segm (1 + 1) by NAT_1:39;
hence card a c= 1 + 1 by A24; :: 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
A25: a = {(union G),[x,(union G)]} and
x in Vertices G ;
card {(union G),[x,(union G)]} <= 2 by CARD_2:50;
then Segm (card {(union G),[x,(union G)]}) c= Segm 2 by NAT_1:39;
hence card a c= 1 + 1 by A25; :: 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 A1, A20; :: thesis: verum