set K = {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} c= [:KEdges,KVertices:]
proof
let x be
object ;
TARSKI:def 3 ( not x in {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} or x in [:KEdges,KVertices:] )
assume
x in {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]}
;
x in [:KEdges,KVertices:]
then x:
(
x = [10,0] or
x = [20,0] or
x = [30,0] or
x = [40,1] or
x = [50,1] or
x = [60,2] or
x = [70,2] )
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;
verum
end;
then reconsider K = {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} as Relation of KEdges,KVertices ;
K is Function-like
proof
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( not [x,y1] in K or not [x,y2] in K or y1 = y2 )
assume
(
[x,y1] in K &
[x,y2] in K )
;
y1 = y2
then
( (
[x,y1] = [10,0] or
[x,y1] = [20,0] or
[x,y1] = [30,0] or
[x,y1] = [40,1] or
[x,y1] = [50,1] or
[x,y1] = [60,2] or
[x,y1] = [70,2] ) & (
[x,y2] = [10,0] or
[x,y2] = [20,0] or
[x,y2] = [30,0] or
[x,y2] = [40,1] or
[x,y2] = [50,1] or
[x,y2] = [60,2] or
[x,y2] = [70,2] ) )
by ENUMSET1:def 5;
then
( ( (
x = 10 &
y1 = 0 ) or (
x = 20 &
y1 = 0 ) or (
x = 30 &
y1 = 0 ) or (
x = 40 &
y1 = 1 ) or (
x = 50 &
y1 = 1 ) or (
x = 60 &
y1 = 2 ) or (
x = 70 &
y1 = 2 ) ) & ( (
x = 10 &
y2 = 0 ) or (
x = 20 &
y2 = 0 ) or (
x = 30 &
y2 = 0 ) or (
x = 40 &
y2 = 1 ) or (
x = 50 &
y2 = 1 ) or (
x = 60 &
y2 = 2 ) or (
x = 70 &
y2 = 2 ) ) )
by XTUPLE_0:1;
hence
y1 = y2
;
verum
end;
then reconsider K = K as PartFunc of KEdges,KVertices ;
dom K = KEdges
then
K is quasi_total
by FUNCT_2:def 1;
hence
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} is Function of KEdges,KVertices
; verum