>PhoX> Sort term.
Sort term defined
>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 intervide U V  =  x ((U x)  (V x)).
intervide =
                                             \U,V  x:U  V x
                                              : ('a  prop)  (
                                                'a  prop)  prop
>PhoX> def inclus A B =  x ((A x)  (B x)).
inclus = \A,B x:A  B x
                                         : ('a  prop)  ('a  prop)  prop
>PhoX> Cst ouvert : (term  prop)  prop.
ouvert : (term  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) :
(term  prop)  prop
>PhoX> goal
>PhoX> A,B (connexe A  connexe B  x ((A x)  (B x))  connexe (union A B)).
Here is the goal:
goal 1/1
    A,B (connexe A  connexe B  x:A  B x  connexe (union A B))

%PhoX% intros.
1 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
    connexe (union A B)

%PhoX% intros.
1 goal created.

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

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

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% intros.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
H6 := A x
    union U V x

%PhoX% elim H4.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
H6 := A x
    union A B x

%PhoX% intro l.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
H6 := A x
    A x

%PhoX% axiom H6.
0 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
    inclus (union A B) U  inclus (union A B) V

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

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% intros.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
H6 := B x
    union U V x

%PhoX% elim H4.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
H6 := B x
    union A B x

%PhoX% intro r.
1 goal created.

goal 1/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
H6 := B x
    B x

%PhoX% axiom H6.
0 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
    inclus (union A B) U  inclus (union A B) V

%PhoX% apply H with H2 and H3 and G and H5.
1 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G1 := inclus A U  inclus A V
    inclus (union A B) U  inclus (union A B) V

%PhoX% apply H0 with H2 and H3 and G0 and H5.
1 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G1 := inclus A U  inclus A V
G2 := inclus B U  inclus B V
    inclus (union A B) U  inclus (union A B) V

%PhoX% left G1.
2 goals created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G2 := inclus B U  inclus B V
H6 := inclus A U
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% left G2.
2 goals created.

goal 2/3
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B U
    inclus (union A B) U  inclus (union A B) V

goal 1/3
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
    inclus (union A B) U  inclus (union A B) V

%PhoX% intro r.
1 goal created.

goal 1/3
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
    inclus (union A B) V

%PhoX% intros.
1 goal created.

goal 1/3
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := union A B x
    V x

%PhoX% left H8.
2 goals created.

goal 2/4
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := A x
    V x

goal 1/4
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := B x
    V x

%PhoX% elim H7.
1 goal created.

goal 1/4
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := B x
    B x

%PhoX% axiom H8.
0 goal created.

goal 3/3
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G2 := inclus B U  inclus B V
H6 := inclus A U
    inclus (union A B) U  inclus (union A B) V

goal 2/3
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B U
    inclus (union A B) U  inclus (union A B) V

goal 1/3
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := A x
    V x

%PhoX% elim H6.
1 goal created.

goal 1/3
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A V
H7 := inclus B V
H8 := A x
    A x

%PhoX% axiom H8.
0 goal created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G2 := inclus B U  inclus B V
H6 := inclus A U
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% left H1.
1 goal created.

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

%PhoX% left H1.
1 goal created.

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

%PhoX% elim H5.
1 goal created.

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

%PhoX% intro 2.
2 goals created.

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

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

%PhoX% elim H7.
1 goal created.

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

%PhoX% axiom H8.
0 goal created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G2 := inclus B U  inclus B V
H6 := inclus A U
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% elim H6.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
G2 := inclus B U  inclus B V
H6 := inclus A U
    inclus (union A B) U  inclus (union A B) V

%PhoX% left G2.
2 goals created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B U
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% left H1.
1 goal created.

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

%PhoX% left H1.
1 goal created.

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

%PhoX% elim H5.
1 goal created.

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

%PhoX% intro 2.
2 goals created.

goal 2/3
H := connexe A
H0 := connexe B
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B V
H1 := A x
H8 := B x
    V ?2

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

%PhoX% elim H6.
1 goal created.

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

%PhoX% axiom H1.
0 goal created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B U
    inclus (union A B) U  inclus (union A B) V

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

%PhoX% elim H7.
1 goal created.

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

%PhoX% axiom H8.
0 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B U
    inclus (union A B) U  inclus (union A B) V

%PhoX% intro l.
1 goal created.

goal 1/1
H := connexe A
H0 := connexe B
H1 := x:A  B x
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B U
    inclus (union A B) U

%PhoX% intros.
1 goal created.

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

%PhoX% left H8.
2 goals created.

goal 2/2
H := connexe A
H0 := connexe B
H1 := x0:A  B x0
H2 := ouvert U
H3 := ouvert V
H4 := inclus (union A B) (union U V)
H5 := intervide U V
G := inclus A (union U V)
G0 := inclus B (union U V)
H6 := inclus A U
H7 := inclus B U
H8 := A x
    U x

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

%PhoX% elim H7.
1 goal created.

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

%PhoX% axiom H8.
0 goal created.

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

%PhoX% elim H6.
1 goal created.

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

%PhoX% axiom H8.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = A,B (connexe A  connexe B  x:A  B x  connexe (union A B))
 : theorem

bye