let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]} or x in [:KEdges,KVertices:] )
assume x in {[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]} ; :: thesis: x in [:KEdges,KVertices:]
then x: ( x = [10,1] or x = [20,2] or x = [30,3] or x = [40,2] or x = [50,2] or x = [60,3] or x = [70,3] ) by ENUMSET1:def 5;
( 10 in KEdges & 20 in KEdges & 30 in KEdges & 40 in KEdges & 50 in KEdges & 60 in KEdges & 70 in KEdges & 0 in KVertices & 1 in KVertices & 2 in KVertices & 3 in KVertices ) by ENUMSET1:def 2, ENUMSET1:def 5;
hence x in [:KEdges,KVertices:] by x, ZFMISC_1:87; :: thesis: verum

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y1] in K or not [x,y2] in K or y1 = y2 )
assume ( [x,y1] in K & [x,y2] in K ) ; :: thesis: y1 = y2
then ( ( [x,y1] = [10,1] or [x,y1] = [20,2] or [x,y1] = [30,3] or [x,y1] = [40,2] or [x,y1] = [50,2] or [x,y1] = [60,3] or [x,y1] = [70,3] ) & ( [x,y2] = [10,1] or [x,y2] = [20,2] or [x,y2] = [30,3] or [x,y2] = [40,2] or [x,y2] = [50,2] or [x,y2] = [60,3] or [x,y2] = [70,3] ) ) by ENUMSET1:def 5;
then ( ( ( x = 10 & y1 = 1 ) or ( x = 20 & y1 = 2 ) or ( x = 30 & y1 = 3 ) or ( x = 40 & y1 = 2 ) or ( x = 50 & y1 = 2 ) or ( x = 60 & y1 = 3 ) or ( x = 70 & y1 = 3 ) ) & ( ( x = 10 & y2 = 1 ) or ( x = 20 & y2 = 2 ) or ( x = 30 & y2 = 3 ) or ( x = 40 & y2 = 2 ) or ( x = 50 & y2 = 2 ) or ( x = 60 & y2 = 3 ) or ( x = 70 & y2 = 3 ) ) ) by XTUPLE_0:1;
hence y1 = y2 ; :: thesis: verum

thus dom K c= KEdges ; :: according to XBOOLE_0:def 10 :: thesis: KEdges c= dom K
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in KEdges or o in dom K )
assume o in KEdges ; :: thesis: o in dom K
then o: ( o = 10 or o = 20 or o = 30 or o = 40 or o = 50 or o = 60 or o = 70 ) by ENUMSET1:def 5;
( [10,1] in K & [20,2] in K & [30,3] in K & [40,2] in K & [50,2] in K & [60,3] in K & [70,3] in K ) by ENUMSET1:def 5;
hence o in dom K by o, XTUPLE_0:def 12; :: thesis: verum