:: AXIOMS semantic presentation
begin
theorem
:: AXIOMS:1
for
X
,
Y
being ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) st ( for
x
,
y
being ( (
real
) (
V28
()
ext-real
real
)
number
) st
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
X
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) &
y
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
Y
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) holds
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
<=
y
: ( (
real
) (
V28
()
ext-real
real
)
number
) ) holds
ex
z
being ( (
real
) (
V28
()
ext-real
real
)
number
) st
for
x
,
y
being ( (
real
) (
V28
()
ext-real
real
)
number
) st
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
X
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) &
y
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
Y
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) holds
(
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
<=
z
: ( (
real
) (
V28
()
ext-real
real
)
number
) &
z
: ( (
real
) (
V28
()
ext-real
real
)
number
)
<=
y
: ( (
real
) (
V28
()
ext-real
real
)
number
) ) ;
theorem
:: AXIOMS:2
for
x
,
y
being ( (
real
) (
V28
()
ext-real
real
)
number
) st
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) &
y
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) holds
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
+
y
: ( (
real
) (
V28
()
ext-real
real
)
number
) : ( ( ) (
V28
()
ext-real
real
)
set
)
in
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ;
theorem
:: AXIOMS:3
for
A
being ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) st
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
in
A
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) & ( for
x
being ( (
real
) (
V28
()
ext-real
real
)
number
) st
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
in
A
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) holds
x
: ( (
real
) (
V28
()
ext-real
real
)
number
)
+
1 : ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) : ( ( ) (
V28
()
ext-real
real
)
set
)
in
A
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) ) holds
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
Subset
of ( ( ) ( )
set
) ) ;
theorem
:: AXIOMS:4
for
k
being ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Nat
) holds
k
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Nat
)
=
{
i
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) where
i
is ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) :
i
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
<
k
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
ext-real
real
)
Nat
)
}
;