>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