```>PhoX> Sort real.
Sort real defined
>PhoX> Cst Infix[5.0] x "<" y : real  real  prop.
\$< : real  real  prop
>PhoX> def Infix[5.0] x ">" y = y < x.
\$> = \x,y (y < x) : real  real  prop
>PhoX> Cst d : real  real  real.
d : real  real  real
>PhoX> Cst R0 : real.
R0 : real
>PhoX> def image f A y =  x ((A x)  (f x) = y).
image =
\f,A,y x:A  f x = y
: ('b  'a)  (
'b  prop)  'a  prop
>PhoX> def inverse f A x = (A (f x)).
inverse = \f,A,x (A (f x))
: ('b  'c)  ('c  'a)  'b  'a
>PhoX> def intervide U V  =   x ((U x)  (V x)).
intervide =
\U,V  x:U  V x
: ('a  prop)  (
'a  prop)  prop
>PhoX> def union U V x = (U x)  (V x).
union = \U,V,x (U x  V x)
: ('a  prop)  ('a  prop)  'a  prop
>PhoX> def inclus A B =  x ((A x)  (B x)).
inclus = \A,B x:A  B x
: ('a  prop)  ('a  prop)  prop
>PhoX> def ouvert O =  x (O x  a > R0 y (d x y < a  O y)).

ouvert = \O x:O  a > R0  y (d x y < a  O y) :
(real  prop)  prop
>PhoX> def connexe A =  U, V (ouvert U  ouvert V  (inclus A (union U

>PhoX> V))  (intervide U V)  (inclus A U)  (inclus A V)).

connexe =
\A
U,V
(ouvert U  ouvert V  inclus A (union U V)
intervide U V  inclus A U  inclus A V) :
(real  prop)  prop
>PhoX> def continue1 f =  x  e > R0 a > R0  y (d x y < a  d (f

>PhoX> x) (f y) < e).
continue1 =
\f
x,e
(e > R0  a > R0  y (d x y < a  d (f x) (f y) < e))
: (real  real)  prop
>PhoX> def continue2 f =  U ((ouvert U)  (ouvert (inverse f U))).

continue2 = \f U:ouvert  ouvert (inverse f U) : (real  real)  prop
>PhoX> lemma lem1 f (continue1 f  continue2 f).
Here is the goal:
goal 1/1
f:continue1  continue2 f

%PhoX% intros.
1 goal created.

goal 1/1
H := continue1 f
continue2 f

%PhoX% intros.
1 goal created.

goal 1/1
H := continue1 f
H0 := ouvert U
ouvert (inverse f U)

%PhoX% intros.
1 goal created.

goal 1/1
H := continue1 f
H0 := ouvert U
H1 := inverse f U x
a > R0  y (d x y < a  inverse f U y)

%PhoX% unfold_hyp H1 inverse.
1 goal created.

goal 1/1
H := continue1 f
H0 := ouvert U
H1 := U (f x)
a > R0  y (d x y < a  inverse f U y)

%PhoX% unfold_hyp H0 ouvert.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a > R0  y (d x0 y < a  U y)
a > R0  y (d x y < a  inverse f U y)

%PhoX% apply H0 with H1.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a > R0  y (d x0 y < a  U y)
G := a > R0  y (d (f x) y < a  U y)
a > R0  y (d x y < a  inverse f U y)

%PhoX% lefts G \$ \$.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a0 > R0  y (d x0 y < a0  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
a0 > R0  y (d x y < a0  inverse f U y)

%PhoX% apply H with H2.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a0 > R0  y (d x0 y < a0  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
G := a0 > R0  y (d ?1 y < a0  d (f ?1) (f y) < a)
a0 > R0  y (d x y < a0  inverse f U y)

%PhoX% lefts G \$ \$.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y (d x0 y < a1  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
H4 := a0 > R0
H5 := y (d ?1 y < a0  d (f ?1) (f y) < a)
a1 > R0  y (d x y < a1  inverse f U y)

%PhoX% intros.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y (d x0 y < a1  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
H4 := a0 > R0
H5 := y (d ?1 y < a0  d (f ?1) (f y) < a)
?2 > R0  y (d x y < ?2  inverse f U y)

%PhoX% intro.
2 goals created.

goal 2/2
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y (d x0 y < a1  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
H4 := a0 > R0
H5 := y (d ?1 y < a0  d (f ?1) (f y) < a)
y (d x y < ?2  inverse f U y)

goal 1/2
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y (d x0 y < a1  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
H4 := a0 > R0
H5 := y (d ?1 y < a0  d (f ?1) (f y) < a)
?2 > R0

%PhoX% axiom H4.
0 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y (d x0 y < a1  U y)
H2 := a > R0
H3 := y (d (f x) y < a  U y)
H4 := a0 > R0
H5 := y (d ?1 y < a0  d (f ?1) (f y) < a)
y (d x y < a0  inverse f U y)

%PhoX% intros.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y0 (d x0 y0 < a1  U y0)
H2 := a > R0
H3 := y0 (d (f x) y0 < a  U y0)
H4 := a0 > R0
H5 := y0 (d ?1 y0 < a0  d (f ?1) (f y0) < a)
H6 := d x y < a0
inverse f U y

%PhoX% elim H3.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y0 (d x0 y0 < a1  U y0)
H2 := a > R0
H3 := y0 (d (f x) y0 < a  U y0)
H4 := a0 > R0
H5 := y0 (d ?1 y0 < a0  d (f ?1) (f y0) < a)
H6 := d x y < a0
d (f x) (f y) < a

%PhoX% elim H5.
1 goal created.

goal 1/1
H := continue1 f
H1 := U (f x)
H0 := x0:U  a1 > R0  y0 (d x0 y0 < a1  U y0)
H2 := a > R0
H3 := y0 (d (f x) y0 < a  U y0)
H4 := a0 > R0
H5 := y0 (d x y0 < a0  d (f x) (f y0) < a)
H6 := d x y < a0
d x y < a0

%PhoX% axiom H6.
0 goal created.

%PhoX% save lem1.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
lem1 = f:continue1  continue2 f : theorem

>PhoX> lemma lem2 f (continue2 f   A (connexe A  connexe (image f A))).
Here is the goal:
goal 1/1
f:continue2  A:connexe  connexe (image f A)

%PhoX% intros.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
connexe (image f A)

%PhoX% intros.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
inclus (image f A) U  inclus (image f A) V

%PhoX% by_absurd.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
inclus (image f A) U  inclus (image f A) V

%PhoX% elim False.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
False

%PhoX% local U' = inverse f U.
U' = inverse f U : real  prop
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
False

%PhoX% local V' = inverse f V.
V' = inverse f V : real  prop
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
False

%PhoX% prove ouvert U'.
2 goals created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
ouvert U'

%PhoX% elim H.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
ouvert U

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
False

%PhoX% prove ouvert V'.
2 goals created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
ouvert V'

%PhoX% elim H.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
ouvert V

%PhoX% axiom H2.
0 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
False

%PhoX% prove inclus A (union U' V').
2 goals created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
inclus A (union U' V')

%PhoX% intros.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
union U' V' x

%PhoX% elim H3.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
image f A (f x)

%PhoX% intros.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
A ?1  f ?1 = f x

%PhoX% intro.
2 goals created.

goal 2/3
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
f ?1 = f x

goal 1/3
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
A ?1

%PhoX% axiom H6.
0 goal created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
H6 := A x
f x = f x

%PhoX% intro.
0 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
False

%PhoX% prove intervide U' V'.
2 goals created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
intervide U' V'

%PhoX% intros.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
H6 := x:U'  V' x
False

%PhoX% elim H4.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
H6 := x:U'  V' x
x:U  V x

%PhoX% left H6.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
H6 := U' x  V' x
x0:U  V x0

%PhoX% intros.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
H6 := U' x  V' x
U ?2  V ?2

%PhoX% axiom H6.
0 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
False

%PhoX% apply H0 with G and G0 and G1 and G2.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
H5 :=  (inclus (image f A) U  inclus (image f A) V)
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
G3 := inclus A U'  inclus A V'
False

%PhoX% rewrite_hyp H5 disjunction.demorgan.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
G3 := inclus A U'  inclus A V'
H5 :=  inclus (image f A) U   inclus (image f A) V
False

%PhoX% left H5.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
G3 := inclus A U'  inclus A V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
False

%PhoX% left G3.
2 goals created.

goal 2/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
False

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A V'
False

%PhoX% elim H6.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A V'
inclus (image f A) V

%PhoX% intros.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A V'
H8 := image f A x
V x

%PhoX% left H8.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A V'
H8 := A x0  f x0 = x
V x

%PhoX% elim H7.
1 goal created.

goal 1/2
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A V'
H8 := A x0  f x0 = x
A x0

%PhoX% elim H8.
0 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
False

%PhoX% elim H5.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
inclus (image f A) U

%PhoX% intros.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
H8 := image f A x
U x

%PhoX% left H8.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
H8 := A x0  f x0 = x
U x

%PhoX% elim H7.
1 goal created.

goal 1/1
H := continue2 f
H0 := connexe A
H1 := ouvert U
H2 := ouvert V
H3 := inclus (image f A) (union U V)
H4 := intervide U V
G := ouvert U'
G0 := ouvert V'
G1 := inclus A (union U' V')
G2 := intervide U' V'
H5 :=  inclus (image f A) U
H6 :=  inclus (image f A) V
H7 := inclus A U'
H8 := A x0  f x0 = x
A x0

%PhoX% elim H8.
0 goal created.

%PhoX% save lem2.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
lem2 = f:continue2  A:connexe  connexe (image f A) : theorem

>PhoX> goal f (continue1 f   A (connexe A  connexe (image f A))).
Here is the goal:
goal 1/1
f:continue1  A:connexe  connexe (image f A)

%PhoX% intro 2.
1 goal created.

goal 1/1
H := continue1 f
A:connexe  connexe (image f A)

%PhoX% elim lem2.
1 goal created.

goal 1/1
H := continue1 f
continue2 f

%PhoX% elim lem1.
1 goal created.

goal 1/1
H := continue1 f
continue1 f

%PhoX% axiom H.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = f:continue1  A:connexe  connexe (image f A) : theorem

bye
```