:: HILBERT1 semantic presentation
begin
definition
let
D
be ( ( ) ( )
set
) ;
attr
D
is
with_VERUM
means
:: HILBERT1:def 1
<*
0
: ( ( ) (
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
in
D
: ( (
V15
() ) (
V15
() )
set
) ;
end;
definition
let
D
be ( ( ) ( )
set
) ;
attr
D
is
with_implication
means
:: HILBERT1:def 2
for
p
,
q
being ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) st
p
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
in
D
: ( (
V15
() ) (
V15
() )
set
) &
q
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
in
D
: ( (
V15
() ) (
V15
() )
set
) holds
(
<*
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
^
p
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
)
: ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
^
q
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) : ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
in
D
: ( (
V15
() ) (
V15
() )
set
) ;
end;
definition
let
D
be ( ( ) ( )
set
) ;
attr
D
is
with_conjunction
means
:: HILBERT1:def 3
for
p
,
q
being ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) st
p
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
in
D
: ( (
V15
() ) (
V15
() )
set
) &
q
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
in
D
: ( (
V15
() ) (
V15
() )
set
) holds
(
<*
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
^
p
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
)
)
: ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
^
q
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
FinSequence
) : ( (
V15
()
Function-like
FinSequence-like
) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
in
D
: ( (
V15
() ) (
V15
() )
set
) ;
end;
definition
let
D
be ( ( ) ( )
set
) ;
attr
D
is
with_propositional_variables
means
:: HILBERT1:def 4
for
n
being ( ( ) (
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) holds
<*
(
3 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
+
n
: ( ( ) (
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( ( ) (
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
in
D
: ( (
V15
() ) (
V15
() )
set
) ;
end;
definition
let
D
be ( ( ) ( )
set
) ;
attr
D
is
HP-closed
means
:: HILBERT1:def 5
(
D
: ( (
V15
() ) (
V15
() )
set
)
c=
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
*
: ( ( ) ( non
empty
functional
FinSequence-membered
)
set
) &
D
: ( (
V15
() ) (
V15
() )
set
) is
with_VERUM
&
D
: ( (
V15
() ) (
V15
() )
set
) is
with_implication
&
D
: ( (
V15
() ) (
V15
() )
set
) is
with_conjunction
&
D
: ( (
V15
() ) (
V15
() )
set
) is
with_propositional_variables
);
end;
registration
cluster
HP-closed
->
non
empty
with_VERUM
with_implication
with_conjunction
with_propositional_variables
for ( ( ) ( )
set
) ;
cluster
with_VERUM
with_implication
with_conjunction
with_propositional_variables
->
HP-closed
for ( ( ) ( )
Element
of
K6
(
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) )
*
)
: ( ( ) ( non
empty
functional
FinSequence-membered
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
end;
definition
func
HP-WFF
->
( ( ) ( )
set
)
means
:: HILBERT1:def 6
(
it
: ( ( ) ( )
set
) is
HP-closed
& ( for
D
being ( ( ) ( )
set
) st
D
: ( ( ) ( )
set
) is
HP-closed
holds
it
: ( ( ) ( )
set
)
c=
D
: ( ( ) ( )
set
) ) );
end;
registration
cluster
HP-WFF
: ( ( ) ( )
set
)
->
HP-closed
;
end;
registration
cluster
non
empty
HP-closed
for ( ( ) ( )
set
) ;
end;
registration
cluster
HP-WFF
: ( ( ) ( non
empty
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
)
->
functional
;
end;
registration
cluster
->
FinSequence-like
for ( ( ) ( )
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) ;
end;
definition
mode
HP-formula
is
( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) ;
end;
definition
func
VERUM
->
( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
equals
:: HILBERT1:def 7
<*
0
: ( ( ) (
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) ;
let
p
,
q
be ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) ;
func
p
=>
q
->
( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
equals
:: HILBERT1:def 8
(
<*
1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
^
p
: ( ( ) ( )
set
)
)
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
^
q
: ( (
V15
()
Function-like
) (
V15
()
Function-like
)
set
) : ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
) ;
func
p
'&'
q
->
( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
equals
:: HILBERT1:def 9
(
<*
2 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
*>
: ( ( ) ( non
empty
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
V19
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
V39
(1 : ( ( ) ( non
empty
V4
()
V5
()
V6
()
V10
() )
Element
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) ) )
FinSequence-like
FinSubsequence-like
)
FinSequence
of
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
^
p
: ( ( ) ( )
set
)
)
: ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
)
^
q
: ( (
V15
()
Function-like
) (
V15
()
Function-like
)
set
) : ( (
V15
()
Function-like
FinSequence-like
) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
set
) ;
end;
definition
let
T
be ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
attr
T
is
Hilbert_theory
means
:: HILBERT1:def 10
(
VERUM
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) & ( for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) &
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) &
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) &
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) &
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) & (
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
T
: ( ( ) ( )
set
) &
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
T
: ( ( ) ( )
set
) implies
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
T
: ( ( ) ( )
set
) ) ) ) );
end;
definition
let
X
be ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
func
CnPos
X
->
( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
means
:: HILBERT1:def 11
for
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
it
: ( (
V15
()
Function-like
) (
V15
()
Function-like
)
set
) iff for
T
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
Hilbert_theory
&
X
: ( ( ) ( )
set
)
c=
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) );
end;
definition
func
HP_TAUT
->
( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
equals
:: HILBERT1:def 12
CnPos
(
{}
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
)
)
: ( ( ) (
empty
proper
V4
()
V5
()
V6
()
V8
()
V9
()
V10
()
Function-like
functional
FinSequence-membered
)
Element
of
K6
(
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: HILBERT1:1
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
VERUM
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:2
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:3
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:4
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:5
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:6
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:7
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:8
for
T
,
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
Hilbert_theory
&
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:9
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:10
for
X
,
Y
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
Y
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
CnPos
Y
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:11
for
X
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
CnPos
(
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
CnPos
X
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
registration
let
X
be ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
cluster
CnPos
X
: ( ( ) (
functional
)
Element
of
K6
(
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
->
Hilbert_theory
;
end;
theorem
:: HILBERT1:12
for
T
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
Hilbert_theory
iff
CnPos
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: HILBERT1:13
for
T
being ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
Hilbert_theory
holds
HP_TAUT
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
T
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
registration
cluster
HP_TAUT
: ( ( ) (
functional
)
Subset
of ( ( ) ( non
empty
)
set
) )
->
Hilbert_theory
;
end;
begin
theorem
:: HILBERT1:14
for
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:15
for
q
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:16
for
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
VERUM
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:17
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:18
for
q
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:19
for
q
,
r
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:20
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:21
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:22
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:23
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:24
for
p
,
q
,
r
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:25
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:26
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:27
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:28
for
q
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:29
for
s
,
q
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
begin
theorem
:: HILBERT1:30
for
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:31
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) iff (
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: HILBERT1:32
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) st
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:33
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:34
for
p
,
q
,
r
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:35
for
r
,
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
r
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:36
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:37
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:38
for
q
,
s
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:39
for
q
,
s
,
p
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:40
for
p
,
s
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:41
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:42
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:43
for
p
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:44
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:45
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:46
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:47
for
p
,
s
,
q
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
(
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:48
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
=>
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:49
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: HILBERT1:50
for
p
,
q
,
s
being ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) ) holds
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
(
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
=>
(
(
p
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
'&'
q
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
'&'
s
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
Element
of
HP-WFF
: ( ( ) ( non
empty
functional
with_VERUM
with_implication
with_conjunction
with_propositional_variables
HP-closed
)
set
) )
)
: ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
) : ( ( ) (
V15
()
V18
(
NAT
: ( ( ) ( non
empty
V4
()
V5
()
V6
() )
Element
of
K6
(
REAL
: ( ( ) ( )
set
) ) : ( ( ) ( non
empty
)
set
) ) )
Function-like
V32
()
FinSequence-like
FinSubsequence-like
)
HP-formula
)
in
HP_TAUT
: ( ( ) (
functional
Hilbert_theory
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;