Grammar vernac vernac := rlemma_cmd [ "RLemma" command:command($a) ":" command:command($b) "." ] -> [ <:vernac:> ]. Grammar vernac vernac := rproperty_cmd [ "RProperty" command:command($a) ":=" command:command($b) "." ] -> [<:vernac:> ]. Grammar vernac vernac := property_cmd [ "Property" command:command($a) ":=" command:command($b) "." ] -> [<:vernac:> ]. Grammar vernac vernac := uremark_cmd [ "URemark" command:command($a) ":" command:command($b) "." ] -> [<:vernac:> ]. Grammar vernac vernac := outremark_cmd [ "OutRemark" command:command($a) ":" command:command($b) "." ] -> [<:vernac:> ]. Chapter basic_definitions. Parameter Ens : Type. (*** that was the only time we refer to Type, thus we avoid ``typical ambiguity'' ***) Parameter IN : Ens -> Ens -> Prop. Parameter AND : Prop -> Prop -> Prop. Axiom AND_conj : (P,Q: Prop) P -> Q -> (AND P Q). Axiom AND_proj1 : (P,Q: Prop) (AND P Q) -> P. Axiom AND_proj2 : (P,Q: Prop) (AND P Q) -> Q. (************ OR *******) Parameter OR : Prop -> Prop -> Prop. Axiom OR_pr1 : (P, Q: Prop) P -> (OR P Q). Axiom OR_pr2 : (P,Q : Prop) Q -> (OR P Q). Axiom OR_pr3 : (P,Q,R:Prop) (P-> R)-> (Q -> R)-> ((OR P Q)-> R). (*****************************************) Definition Apply0 := [P: Prop] P. Definition Apply1 := [P: Ens -> Prop][X: Ens](P X). Definition Apply2 := [P: Ens-> Ens -> Prop][X, Y: Ens](P X Y). Definition Apply3 := [P: Ens-> Ens -> Ens -> Prop][X,Y,Z: Ens](P X Y Z). Definition TRUE := (P: Prop) P -> P. Definition True0 := [P: Prop][p:P]p. Definition True1 := [X: Ens]True0. Definition True2 := [X,Y: Ens]True0. Definition Look_at := [A: Ens]TRUE. Definition Just_look_at := True1. Definition Try_conclude := [P: Prop]P -> P. Definition Triv := [P: Prop][p: P] p. Definition Consider0 := [P: Prop]TRUE. Definition Consider1 := [P: Ens -> Prop]TRUE. Definition Consider2 := [P: Ens->Ens->Prop]TRUE. Definition Just_consider0 := [P: Prop]True0. Definition Just_consider1 := [P: Ens -> Prop]True0. Definition Just_consider2 := [P: Ens->Ens->Prop]True0. Property Imply := [P,Q: Prop](Apply0 P) -> (Apply0 Q). Lemma apply_Imply : (P, Q : Prop)( Imply P Q ) -> ( Apply0 P ) -> ( Apply0 Q ). Proof [P, Q : Prop][ hyp : ( Imply P Q )] [ h00001 : ( Apply0 P )] ( hyp h00001 ). Section OR_lem1A. Variables P,Q: Prop. Hypothesis c : (Consider0 (OR P Q)). Hypothesis p: (Apply0 P). OutRemark orlem1_out : (OR P Q). Proof (OR_pr1 P Q p). End OR_lem1A. Lemma OR_lem1 : (P, Q : Prop)( Consider0 ( OR P Q ) ) -> ( Apply0 P ) -> ( OR P Q ). Proof [P, Q : Prop][c : ( Consider0 ( OR P Q ) )] [p : ( Apply0 P )] (orlem1_out P Q p). Section OR_lem2A. Variables P,Q: Prop. Hypothesis c : (Consider0 (OR P Q)). Hypothesis q: (Apply0 Q). OutRemark orlem2_out : (OR P Q). Proof (OR_pr2 P Q q). End OR_lem2A. Lemma OR_lem2 : (P, Q : Prop)( Consider0 ( OR P Q ) ) -> ( Apply0 Q ) -> ( OR P Q ). Proof [P, Q : Prop][c : ( Consider0 ( OR P Q ) )] [q : ( Apply0 Q )] (orlem2_out P Q q). Section OR_lem3A. Variables P,Q,R: Prop. Hypothesis i : (Imply P R). Hypothesis j : (Imply Q R). Hypothesis o: (OR P Q). OutRemark orlem3_out : R. Proof (OR_pr3 P Q R i j o). End OR_lem3A. Lemma OR_lem3 : (P, Q, R : Prop)( Imply P R ) -> ( Imply Q R ) -> ( OR P Q ) -> R. Proof [P, Q, R : Prop][i : ( Imply P R )] [j : ( Imply Q R )] [o : ( OR P Q )] (orlem3_out P Q R i j o). Parameter FALSE : Prop. Axiom false_implies_everythingA : (P: Prop) FALSE -> P. Lemma false_implies_everything : (P: Prop)(Try_conclude P) -> FALSE -> P. Proof [P: Prop][h:(Try_conclude P)][f: FALSE] (false_implies_everythingA P f). Property NOT := [P: Prop]P -> FALSE. Lemma apply_NOT : (P: Prop)(NOT P) -> (Apply0 P) -> FALSE. Proof [P: Prop][n: (NOT P)][a : (Apply0 P)](n a). Axiom excluded_middleA: (P: Prop)(NOT (NOT P))-> P. Lemma excluded_middle : (P: Prop)(NOT (NOT P)) -> P. Proof excluded_middleA. Chapter subset_and_equality. Property SUB := [A,B: Ens] (C: Ens) (IN C A) -> (IN C B). Property EQ := [A,B: Ens] (AND (SUB A B) (SUB B A)). Lemma apply_SUB : ( A, B, C : Ens) ( SUB A B ) -> ( IN C A ) -> ( IN C B ). Proof [ A, B, C : Ens] [ hyp : ( SUB A B )] [ h00001 : ( IN C A )] ( hyp C h00001 ). Lemma conj_EQ : ( A, B : Ens) ( SUB A B ) -> ( SUB B A ) -> ( EQ A B ). Proof [ A, B : Ens] [ hyp1 : ( SUB A B )] [ hyp2 : (SUB B A )] (AND_conj ( SUB A B ) (SUB B A ) hyp1 hyp2). Lemma proj1_EQ : ( A, B : Ens) ( EQ A B ) -> ( SUB A B ). Proof [ A, B : Ens] [ hyp : ( EQ A B )] (AND_proj1 ( SUB A B ) (SUB B A ) hyp). Lemma proj2_EQ : ( A, B : Ens) ( EQ A B ) -> ( SUB B A ). Proof [ A, B : Ens] [ hyp : ( EQ A B )] (AND_proj2 ( SUB A B ) (SUB B A ) hyp). Section SUB_transA . Variables A , B , C : Ens . Hypothesis i : (SUB A B) . Hypothesis j : (SUB B C) . Section SUB_trans1 . Variable X : Ens . Hypothesis x : (IN X A) . Remark automatic_00001 : (IN X B) . Proof (apply_SUB A B X i x) . Theorem automatic_00002 : (IN X C) . Proof (apply_SUB B C X j automatic_00001) . End SUB_trans1 . Remark THM_SUB_trans1 : (X : Ens) (IN X A) -> (IN X C) . Proof automatic_00002 . Theorem SUB_trans_out : (SUB A C) . Proof THM_SUB_trans1 . End SUB_transA. Lemma SUB_trans : (A, B, C : Ens) ( SUB A B ) -> ( SUB B C ) -> ( SUB A C ). Proof SUB_trans_out. Section sub_refl . Variable A : Ens . Section sub_refl1 . Variable X : Ens . Hypothesis x : (IN X A) . Theorem sub_refl1_out : (IN X A) . Proof x . End sub_refl1 . Remark THM_sub_refl1 : (X : Ens) (IN X A) -> (IN X A) . Proof sub_refl1_out . Theorem sub_refl_out : (SUB A A) . Proof THM_sub_refl1 . End sub_refl. Theorem SUB_refl : (A : Ens) ( SUB A A ). Proof sub_refl_out. Section EQ_reflA . Variable A : Ens . Remark step1 : (SUB A A) . Proof (SUB_refl A) . Theorem automatic_00003 : (EQ A A) . Proof (conj_EQ A A step1 step1) . End EQ_reflA. Theorem EQ_refl : (A : Ens) ( EQ A A ). Proof automatic_00003. Section EQ_symmA . Variables A , B : Ens . Hypothesis i : (EQ A B) . Remark automatic_00004 : (SUB A B) . Proof (proj1_EQ A B i) . Remark automatic_00005 : (SUB B A) . Proof (proj2_EQ A B i) . Theorem automatic_00006 : (EQ B A) . Proof (conj_EQ B A automatic_00005 automatic_00004) . End EQ_symmA. Lemma EQ_symm : (A, B : Ens) ( EQ A B ) -> ( EQ B A ). Proof automatic_00006. Section EQ_transA . Variables A , B , C : Ens . Hypothesis i : (EQ A B) . Hypothesis j : (EQ B C) . Remark automatic_00007 : (SUB A B) . Proof (proj1_EQ A B i) . Remark automatic_00008 : (SUB B C) . Proof (proj1_EQ B C j) . Remark automatic_00009 : (SUB B A) . Proof (proj2_EQ A B i) . Remark automatic_00010 : (SUB C B) . Proof (proj2_EQ B C j) . Remark automatic_00014 : (SUB A C) . Proof (SUB_trans A B C automatic_00007 automatic_00008) . Remark automatic_00017 : (SUB C A) . Proof (SUB_trans C B A automatic_00010 automatic_00009) . Theorem automatic_00019 : (EQ A C) . Proof (conj_EQ A C automatic_00014 automatic_00017) . End EQ_transA. Lemma EQ_trans : (A, B, C : Ens) ( EQ A B ) -> ( EQ B C ) -> ( EQ A C ). Proof automatic_00019. Chapter existence. Property DOESNT_EXIST := [P: Ens -> Prop](X: Ens)(P X) -> FALSE. Lemma apply_DOESNT_EXIST : (P: Ens -> Prop)(X: Ens) (DOESNT_EXIST P)-> (Apply1 P X) -> FALSE. Proof [P: Ens -> Prop][X: Ens][h: (DOESNT_EXIST P)][a: (Apply1 P X)] (h X a). Property EXISTS := [P: Ens -> Prop](NOT (DOESNT_EXIST P)). Lemma apply_EXISTS : (P: Ens-> Prop)(EXISTS P) -> (NOT (DOESNT_EXIST P)). Proof [P: Ens->Prop][e: (EXISTS P)]e. Section apply_EXISTS2A. Variable P : Ens -> Prop. Hypothesis e: (EXISTS P). Hypothesis f: (DOESNT_EXIST P). Fact automatic_00001 : ( NOT ( DOESNT_EXIST P ) ). Proof ( apply_EXISTS P e ). Fact user_00001 : (Apply0 (DOESNT_EXIST P)). Proof f. Theorem automatic_00020 : ( FALSE ). Proof ( apply_NOT ( DOESNT_EXIST P ) automatic_00001 user_00001 ). End apply_EXISTS2A. Theorem THM_apply_EXISTS2A : (P : Ens-> Prop) ( EXISTS P ) -> ( DOESNT_EXIST P ) -> ( FALSE ). Proof automatic_00020. Section EXISTS_th1A. Variable P: Ens -> Prop. Variable X: Ens. Hypothesis x: (P X). Fact user3 : (Apply1 P X). Proof x. Section EXISTS_th1B. Hypothesis h: (DOESNT_EXIST P). Theorem automatic_00021 : ( FALSE ). Proof ( apply_DOESNT_EXIST P X h user3 ). End EXISTS_th1B. Fact THM_EXISTS_th1B : ( DOESNT_EXIST P ) -> ( FALSE ). Proof automatic_00021. Theorem user4: (EXISTS P). Proof THM_EXISTS_th1B. End EXISTS_th1A. Lemma EXISTS_th1 : (P: Ens -> Prop)( X : Ens) (Apply1 P X ) -> ( EXISTS P ). Proof user4. Chapter other_axioms. (********* the axiom of choice, applied to the whole Ens *******) Parameter CHOICE : (P: Ens -> Prop) Ens. Axiom CHOICE_pr : (P: Ens -> Prop)(EXISTS P)-> (P (CHOICE P)). Lemma CHOICE_lem1 : (P: Ens -> Prop)(EXISTS P)-> (P (CHOICE P)). Proof CHOICE_pr. (**** we need to assume that something EXISTS, for simplicity assume the emptyset *****) Parameter Zero : Ens. Axiom Zero_pr : (X: Ens)(IN X Zero) -> FALSE. Lemma Zero_lem1 : (X: Ens)(IN X Zero) -> FALSE. Proof Zero_pr. (********* we have to define Bounded *********************) Property bounds := [P: Ens -> Prop] [A : Ens] (X: Ens) (Apply1 P X) -> (IN X A). Lemma apply_bounds : (P : Ens -> Prop)(A, X : Ens) ( bounds P A ) -> (Apply1 P X ) -> ( IN X A ). Proof [P : Ens -> Prop][A, X : Ens][ hyp : ( bounds P A )] [ h00001 : ( P X )] ( hyp X h00001 ). Property is_bounded := [P : Ens -> Prop] (EXISTS (bounds P) ). Lemma apply_is_bounded : (P : Ens -> Prop)( is_bounded P ) -> ( EXISTS ( bounds P ) ). Proof [P : Ens -> Prop][ hyp : ( is_bounded P )] ( hyp ). (********** unions of two sets, then big Unions ************) Parameter union : (A,B: Ens) Ens. Axiom union_pr1 : (A, B: Ens) (SUB A (union A B)). Axiom union_pr2 : (A,B : Ens) (SUB B (union A B)). Axiom union_pr3 : (A, B, C: Ens) (SUB A C)-> (SUB B C) -> (SUB (union A B) C). Section union_lem1A. Variables A,B: Ens. Hypothesis l: (Look_at (union A B)). OutRemark unionlem1 : (SUB A (union A B)). Proof (union_pr1 A B). End union_lem1A. Lemma union_lem1 : (A, B : Ens)( Look_at ( union A B ) ) -> ( SUB A ( union A B ) ). Proof [A, B : Ens][l : ( Look_at ( union A B ) )] (unionlem1 A B). Section union_lem2A. Variables A,B: Ens. Hypothesis l: (Look_at (union A B)). OutRemark unionlem2 : (SUB B (union A B)). Proof (union_pr2 A B). End union_lem2A. Lemma union_lem2 : (A, B : Ens)( Look_at ( union A B ) ) -> ( SUB B ( union A B ) ). Proof [A, B : Ens][l : ( Look_at ( union A B ) )] (unionlem2 A B). Lemma union_lem3 : (A, B, C: Ens) (SUB A C)-> (SUB B C) ->(Look_at (union A B))-> (SUB (union A B) C). Proof [A,B,C: Ens][h:(SUB A C)][i:(SUB B C)][k:(Look_at (union A B))] (union_pr3 A B C h i). Property nested_in := [A,B,C: Ens] (AND (IN A B) (IN B C)). Lemma conj_nested_in : ( A, B, C : Ens) ( IN A B ) -> ( IN B C ) -> ( nested_in A B C ). Proof [ A, B, C : Ens] [ hyp1 : ( IN A B )] [ hyp2 : (IN B C )] (AND_conj ( IN A B ) (IN B C ) hyp1 hyp2). Lemma proj1_nested_in : ( A, B, C : Ens) ( nested_in A B C ) -> ( IN A B ). Proof [ A, B, C : Ens] [ hyp : ( nested_in A B C )] (AND_proj1 ( IN A B ) (IN B C ) hyp). Lemma proj2_nested_in : ( A, B, C : Ens) ( nested_in A B C ) -> ( IN B C ). Proof [ A, B, C : Ens] [ hyp : ( nested_in A B C )] (AND_proj2 ( IN A B ) (IN B C ) hyp). Property b_in_bigunion_a := [A,B: Ens] (EXISTS ([C: Ens] (nested_in B C A))). Lemma apply_b_in_bigunion_a : (A, B : Ens)( b_in_bigunion_a A B ) -> (EXISTS ( [ C : Ens ] ( nested_in B C A ) ) ). Proof [A, B : Ens][ hyp : ( b_in_bigunion_a A B )] ( hyp ). Axiom Union_boundedA : (F : Ens) (is_bounded (b_in_bigunion_a F)). Lemma Union_bounded : (F : Ens) (is_bounded (b_in_bigunion_a F)). Proof Union_boundedA. (******** singletons ****************) Parameter Singleton : Ens -> Ens. Axiom Singleton_pr1 : (X : Ens) (Look_at (Singleton X))->(IN X (Singleton X)). Axiom Singleton_pr2 : (X: Ens)(Y: Ens) (IN Y (Singleton X)) -> (EQ X Y). Lemma Singleton_lem1 : (X : Ens) (Look_at (Singleton X))->(IN X (Singleton X)). Proof Singleton_pr1. Lemma Singleton_lem2 : (X,Y: Ens)(IN Y (Singleton X)) -> (EQ X Y). Proof Singleton_pr2. (********* powerset ******************) Axiom Powerset_Bounded : (X: Ens) (is_bounded ([Y: Ens] (SUB Y X))). (********* replacement axioms *********) Parameter REPLACEMENT : (P: Ens -> Prop) Ens. Axiom REPLACEMENT_pr1 : (P: Ens -> Prop)(X: Ens)(is_bounded P)-> (P X) -> (IN X (REPLACEMENT P)). Lemma replacement_lem1 : (P: Ens -> Prop)(X: Ens)(is_bounded P)-> (Apply1 P X) -> (IN X (REPLACEMENT P)). Proof REPLACEMENT_pr1. Axiom REPLACEMENT_pr2 : (P: Ens -> Prop)(X: Ens)(is_bounded P)-> (IN X (REPLACEMENT P)) -> (P X). Lemma replacement_lem2 : (P: Ens -> Prop)(X: Ens)(is_bounded P)-> (IN X (REPLACEMENT P)) -> (P X). Proof REPLACEMENT_pr2. (*********** for the natural numbers ***********) Definition Next := [X : Ens] (union X (Singleton X)). Property closed_for_next := [X: Ens] (A: Ens) (IN A X) -> (IN (Next A) X). Lemma apply_closed_for_next : (X, A : Ens)( closed_for_next X ) -> ( IN A X ) -> ( IN ( Next A ) X ). Proof [X, A : Ens][ hyp : ( closed_for_next X )] [ h00001 : ( IN A X )] ( hyp A h00001 ). Property contains_nn := [X: Ens] (AND (IN Zero X) (closed_for_next X)). Lemma conj_contains_nn : ( X : Ens) ( IN Zero X ) -> ( closed_for_next X ) -> ( contains_nn X ). Proof [ X : Ens] [ hyp1 : ( IN Zero X )] [ hyp2 : (closed_for_next X )] (AND_conj ( IN Zero X ) (closed_for_next X ) hyp1 hyp2). Lemma proj1_contains_nn : ( X : Ens) ( contains_nn X ) -> ( IN Zero X ). Proof [ X : Ens] [ hyp : ( contains_nn X )] (AND_proj1 ( IN Zero X ) (closed_for_next X ) hyp). Lemma proj2_contains_nn : ( X : Ens) ( contains_nn X ) -> ( closed_for_next X ). Proof [ X : Ens] [ hyp : ( contains_nn X )] (AND_proj2 ( IN Zero X ) (closed_for_next X ) hyp). Axiom Infinity_Exists : (EXISTS contains_nn). (****************************************************************) (************** beyond this point the words Axiom, Parameter, ***) (************** Declare don't occur **************************) (****************************************************************) Chapter first_results. Property is_empty := [Z: Ens] (X: Ens) (IN X Z) -> FALSE. Lemma apply_is_empty : (Z, X : Ens)( is_empty Z ) -> ( IN X Z ) -> ( FALSE ). Proof [Z, X : Ens][ hyp : ( is_empty Z )] [ h00001 : ( IN X Z )] ( hyp X h00001 ). Section is_empty_ZeroA. Variable X: Ens. Hypothesis x: (IN X Zero). Theorem automatic_00024 : ( FALSE ). Proof ( Zero_lem1 X x ). End is_empty_ZeroA. Fact is_empty_Zero : (is_empty Zero). Proof [X : Ens][x : ( IN X Zero )] (automatic_00024 X x). Section is_empty_th1A. Variables Z,A: Ens. Hypothesis z: (is_empty Z). Hypothesis a: (Look_at A). Section is_empty_th1B. Variable X: Ens. Hypothesis x: (IN X Z). Fact automatic_00025 : ( FALSE ). Proof ( apply_is_empty Z X z x ). Fact user_00025 : (Try_conclude (IN X A)). Proof (Triv (IN X A)). Theorem automatic_00026 : ( IN X A ). Proof ( false_implies_everything ( IN X A ) user_00025 automatic_00025 ). End is_empty_th1B. Theorem THM_is_empty_th1B : (SUB Z A). Proof [X : Ens][x : ( IN X Z )] (automatic_00026 X x). End is_empty_th1A. Lemma is_empty_th1 : (Z, A : Ens)( is_empty Z ) -> ( Look_at A ) -> ( SUB Z A ). Proof [Z, A : Ens][z : ( is_empty Z )] [a : ( Look_at A )] (THM_is_empty_th1B Z A z). Section is_empty_uniA. Variable Z: Ens. Hypothesis z: (is_empty Z). Fact user_00026 : (Look_at Z). Proof (Just_look_at Z). Fact user_00027 : (Look_at Zero). Proof (Just_look_at Zero). Fact automatic_00028 : ( SUB Zero Z ). Proof ( is_empty_th1 Zero Z is_empty_Zero user_00026 ). Fact automatic_00029 : ( SUB Z Zero ). Proof ( is_empty_th1 Z Zero z user_00027 ). Theorem automatic_00030 : ( EQ Z Zero ). Proof ( conj_EQ Z Zero automatic_00029 automatic_00028 ). End is_empty_uniA. Theorem is_empty_uni : (Z : Ens)( is_empty Z ) -> ( EQ Z Zero ). Proof [Z : Ens][z : ( is_empty Z )] (automatic_00030 Z z). Property is_nonempty := [A: Ens](is_empty A) -> FALSE. Lemma apply_is_nonempty : (A : Ens)( is_nonempty A ) -> ( is_empty A ) -> ( FALSE ). Proof [A : Ens][ hyp : ( is_nonempty A )] [ h00001 : ( is_empty A )] ( hyp h00001 ). Section is_nonempty_th1A. Variables A,X: Ens. Hypothesis x : (IN X A). Section is_nonempty_th1B. Hypothesis i: (is_empty A). Theorem automatic_00031 : ( FALSE ). Proof ( apply_is_empty A X i x ). End is_nonempty_th1B. Theorem THM_is_nonempty_th1B : ( is_nonempty A ). Proof [i : ( is_empty A )] (automatic_00031 i). End is_nonempty_th1A. Lemma is_nonempty_th1 : (A, X : Ens)( IN X A ) -> ( is_nonempty A ). Proof [A, X : Ens][x : ( IN X A )] (THM_is_nonempty_th1B A X x). Property element_of := [A,B: Ens] (IN B A). Lemma apply_element_of : (A, B : Ens)( element_of A B ) -> ( IN B A ). Proof [A, B : Ens][ hyp : ( element_of A B )] ( hyp ). Definition Something_in := [A: Ens] (CHOICE (element_of A)). Section is_nonempty_th2A. Variable A : Ens. Hypothesis i : (is_nonempty A). Section is_nonempty_th2Z. Section is_nonempty_th2B. Hypothesis e : (DOESNT_EXIST (element_of A)). Section is_nonempty_th2C. Variable X: Ens. Hypothesis x : (IN X A). Remark user_00128 : (Apply1 (element_of A) X). Proof x. OutRemark automatic_00129 : FALSE . Proof ( apply_DOESNT_EXIST ( element_of A ) X e user_00128 ). End is_nonempty_th2C. Remark autout_00130 : (is_empty A). Proof automatic_00129. OutRemark automatic_00130 : FALSE . Proof ( apply_is_nonempty A i autout_00130 ). End is_nonempty_th2B. OutRemark autout_00131 : (NOT ( DOESNT_EXIST ( element_of A ) )). Proof automatic_00130. End is_nonempty_th2Z. Remark autout_00131a : (EXISTS ( element_of A )). Proof autout_00131. Remark automatic_00132 : (element_of A ( CHOICE ( element_of A ) ) ). Proof ( CHOICE_lem1 ( element_of A ) autout_00131a ). Remark automatic_00135 : (IN ( CHOICE ( element_of A ) ) A ). Proof ( apply_element_of A ( CHOICE ( element_of A ) ) automatic_00132 ). OutRemark user_00135 : (IN (Something_in A) A). Proof automatic_00135. End is_nonempty_th2A. Lemma is_nonempty_th2 : (A : Ens)( is_nonempty A ) -> ( IN ( Something_in A ) A ). Proof [A : Ens][i : ( is_nonempty A )] (user_00135 A i). Property NEQ := [A,B: Ens] (EQ A B) -> FALSE. Lemma apply_NEQ : (A, B : Ens)( NEQ A B ) -> ( EQ A B ) -> ( FALSE ). Proof [A, B : Ens][ hyp : ( NEQ A B )] [ h00001 : ( EQ A B )] ( hyp h00001 ). Property strictSUB := [A,B: Ens] (AND (SUB A B) (NEQ A B)). Lemma conj_strictSUB : (A, B : Ens)( SUB A B ) -> ( NEQ A B ) -> ( strictSUB A B ). Proof [A, B : Ens][ hyp1 : ( SUB A B ) ] [ hyp2 : ( NEQ A B ) ] (AND_conj ( SUB A B )( NEQ A B ) hyp1 hyp2). Lemma proj1_strictSUB : (A, B : Ens)( strictSUB A B ) -> ( SUB A B ) . Proof [A, B : Ens][ hyp : ( strictSUB A B )] (AND_proj1 ( SUB A B ) ( NEQ A B ) hyp). Lemma proj2_strictSUB : (A, B : Ens)( strictSUB A B ) -> ( NEQ A B ) . Proof [A, B : Ens][ hyp : ( strictSUB A B )] (AND_proj2 ( SUB A B ) ( NEQ A B ) hyp). Section NEQ_symmA. Variables A,B: Ens. Hypothesis i: (NEQ A B). Section NEQ_symmB. Hypothesis j: (EQ B A). Fact automatic_00034 : ( EQ A B ). Proof ( EQ_symm B A j ). Theorem automatic_00041 : ( FALSE ). Proof ( apply_NEQ A B i automatic_00034 ). End NEQ_symmB. Theorem THM_NEQ_symmB : ( NEQ B A ). Proof [j : ( EQ B A )] (automatic_00041 j). End NEQ_symmA. Lemma NEQ_symm : (A, B : Ens)( NEQ A B ) -> ( NEQ B A ). Proof [A, B : Ens][i : ( NEQ A B )] (THM_NEQ_symmB A B i). Section strictSUB_trans1A. Variables A,B,C: Ens. Hypothesis i: (strictSUB A B). Hypothesis j: (SUB B C). Fact automatic_00042 : ( SUB A B ). Proof ( proj1_strictSUB A B i ). Fact automatic_00043 : ( NEQ A B ). Proof ( proj2_strictSUB A B i ). Fact automatic_00044 : ( SUB A C ). Proof ( SUB_trans A B C automatic_00042 j ). Section strictSUB_trans1B. Hypothesis k: (EQ A C). Fact automatic_00045 : ( SUB C A ). Proof ( proj2_EQ A C k ). Fact automatic_00046 : ( EQ C A ). Proof ( EQ_symm A C k ). Fact automatic_00047 : ( NEQ B A ). Proof ( NEQ_symm A B automatic_00043 ). Fact automatic_00048 : ( SUB A A ). Proof ( SUB_trans A C A automatic_00044 automatic_00045 ). Fact automatic_00049 : ( SUB B A ). Proof ( SUB_trans B C A j automatic_00045 ). Fact automatic_00050 : ( SUB C B ). Proof ( SUB_trans C A B automatic_00045 automatic_00042 ). Fact automatic_00051 : ( SUB C C ). Proof ( SUB_trans C A C automatic_00045 automatic_00044 ). Fact automatic_00052 : ( EQ A A ). Proof ( EQ_trans A C A k automatic_00046 ). Fact automatic_00053 : ( EQ C C ). Proof ( EQ_trans C A C automatic_00046 k ). Fact automatic_00054 : ( EQ A B ). Proof ( conj_EQ A B automatic_00042 automatic_00049 ). Fact automatic_00055 : ( EQ B A ). Proof ( conj_EQ B A automatic_00049 automatic_00042 ). Fact automatic_00056 : ( EQ B C ). Proof ( conj_EQ B C j automatic_00050 ). Fact automatic_00057 : ( EQ C B ). Proof ( conj_EQ C B automatic_00050 j ). Fact automatic_00058 : ( SUB B B ). Proof ( SUB_trans B A B automatic_00049 automatic_00042 ). Fact automatic_00059 : ( SUB B B ). Proof ( SUB_trans B C B j automatic_00050 ). Fact automatic_00060 : ( strictSUB B A ). Proof ( conj_strictSUB B A automatic_00049 automatic_00047 ). Theorem automatic_00064 : ( FALSE ). Proof ( apply_NEQ A B automatic_00043 automatic_00054 ). End strictSUB_trans1B. Fact THM_strictSUB_trans1B : ( NEQ A C ). Proof [k : ( EQ A C )] (automatic_00064 k). Theorem automatic_00065 : ( strictSUB A C ). Proof ( conj_strictSUB A C automatic_00044 THM_strictSUB_trans1B ). End strictSUB_trans1A. Lemma strictSUB_trans1 : (A, B, C : Ens)( strictSUB A B ) -> ( SUB B C ) -> ( strictSUB A C ). Proof [A, B, C : Ens][i : ( strictSUB A B )] [j : ( SUB B C )] (automatic_00065 A B C i j). Section strictSUB_trans2A. Variables A,B,C: Ens. Hypothesis i: (SUB A B). Hypothesis j: (strictSUB B C). Fact automatic_00071 : ( SUB B C ). Proof ( proj1_strictSUB B C j ). Fact automatic_00072 : ( NEQ B C ). Proof ( proj2_strictSUB B C j ). Fact automatic_00073 : ( SUB A C ). Proof ( SUB_trans A B C i automatic_00071 ). Remark automatic_00074 : ( NEQ C B ). Proof ( NEQ_symm B C automatic_00072 ). Section strictSUB_trans2B. Hypothesis h: (EQ A C). Fact automatic_00075 : ( SUB C A ). Proof ( proj2_EQ A C h ). Fact automatic_00076 : ( EQ C A ). Proof ( EQ_symm A C h ). Remark automatic_00077 : ( SUB A A ). Proof ( SUB_trans A C A automatic_00073 automatic_00075 ). Fact automatic_00078 : ( SUB B A ). Proof ( SUB_trans B C A automatic_00071 automatic_00075 ). Fact automatic_00079 : ( SUB C B ). Proof ( SUB_trans C A B automatic_00075 i ). Remark automatic_00080 : ( SUB C C ). Proof ( SUB_trans C A C automatic_00075 automatic_00073 ). Remark automatic_00081 : ( EQ A A ). Proof ( EQ_trans A C A h automatic_00076 ). Remark automatic_00082 : ( EQ C C ). Proof ( EQ_trans C A C automatic_00076 h ). Remark automatic_00083 : ( strictSUB B A ). Proof ( strictSUB_trans1 B C A j automatic_00075 ). Fact automatic_00086 : ( EQ B C ). Proof ( conj_EQ B C automatic_00071 automatic_00079 ). Theorem automatic_00094 : ( FALSE ). Proof ( apply_NEQ B C automatic_00072 automatic_00086 ). End strictSUB_trans2B. Fact THM_strictSUB_trans2B : ( NEQ A C ). Proof [h : ( EQ A C )] (automatic_00094 h). Theorem automatic_00095 : ( strictSUB A C ). Proof ( conj_strictSUB A C automatic_00073 THM_strictSUB_trans2B ). End strictSUB_trans2A. Theorem THM_strictSUB_trans2A : (A, B, C : Ens)( SUB A B ) -> ( strictSUB B C ) -> ( strictSUB A C ). Proof [A, B, C : Ens][i : ( SUB A B )] [j : ( strictSUB B C )] (automatic_00095 A B C i j). Section bounded_th1A. Variable P: Ens -> Prop. Variable A : Ens. Hypothesis b: (bounds P A). Fact user_00095 : (Apply1 (bounds P) A). Proof b. Fact automatic_00096 : ( EXISTS ( bounds P ) ). Proof ( EXISTS_th1 ( bounds P ) A user_00095 ). Theorem user_00096 : (is_bounded P). Proof automatic_00096. End bounded_th1A. Lemma bounded_th1 : (P : Ens -> Prop)(A : Ens) ( bounds P A ) -> ( is_bounded P ). Proof [P : Ens -> Prop][A : Ens][b : ( bounds P A )] (user_00096 P A b). Property Restriction := [P: Ens -> Prop][A,X: Ens](AND (IN X A) (P X)). Lemma conj_Restriction : (P : Ens -> Prop)(A, X : Ens) ( IN X A ) -> ( P X ) -> ( Restriction P A X ). Proof [P : Ens -> Prop][A, X : Ens][ hyp1 : ( IN X A ) ] [ hyp2 : ( P X ) ] (AND_conj ( IN X A )( P X ) hyp1 hyp2). Lemma proj1_Restriction : (P : Ens -> Prop)(A, X : Ens)( Restriction P A X ) -> ( IN X A ) . Proof [P : Ens -> Prop][A, X : Ens][ hyp : ( Restriction P A X )] (AND_proj1 ( IN X A ) ( P X ) hyp). Lemma proj2_Restriction : (P : Ens -> Prop)(A, X : Ens)( Restriction P A X ) -> ( P X ) . Proof [P : Ens -> Prop][A, X : Ens][ hyp : ( Restriction P A X )] (AND_proj2 ( IN X A ) ( P X ) hyp). Section Restriction_boundedA. Variable P: Ens-> Prop. Variable A : Ens. Hypothesis a : (Consider1 (Restriction P A)). Section Restriction_boundedB. Variable X : Ens. Hypothesis h : ((Restriction P A) X). Fact user_00094 : (Restriction P A X). Proof h. Theorem automatic_00097 : ( IN X A ). Proof ( proj1_Restriction P A X user_00094 ). End Restriction_boundedB. Fact THM_Restriction_boundedB : (bounds (Restriction P A) A). Proof [X : Ens][h : ( ( Restriction P A ) X )] (automatic_00097 X h). OutRemark automatic_00098 : ( is_bounded ( Restriction P A ) ). Proof ( bounded_th1 ( Restriction P A ) A THM_Restriction_boundedB ). End Restriction_boundedA. Lemma Restriction_bounded : (P : Ens -> Prop) (A : Ens)( Consider1 ( Restriction P A ) ) -> ( is_bounded ( Restriction P A ) ). Proof [P : Ens -> Prop][A : Ens][a : ( Consider1 ( Restriction P A ) )] (automatic_00098 P A). Definition Set_Of := [A: Ens][P: Ens -> Prop] (REPLACEMENT (Restriction P A)). Section set_of_th1A. Variables A,X: Ens. Variable P: Ens-> Prop. Hypothesis h : (Look_at (Set_Of A P)). Hypothesis k: (IN X A). Hypothesis l: (P X). Remark automatic_00100 : (Restriction P A X ). Proof ( conj_Restriction P A X k l ). Remark user_00100 : (Consider1 (Restriction P A)). Proof (Just_consider1 (Restriction P A)). Remark automatic_00101 : (is_bounded ( Restriction P A ) ). Proof ( Restriction_bounded P A user_00100 ). Remark user_00101 : (Apply1 (Restriction P A) X). Proof automatic_00100. Remark automatic_00104 : (IN X ( REPLACEMENT ( Restriction P A ) ) ). Proof ( replacement_lem1 ( Restriction P A ) X automatic_00101 user_00101 ). OutRemark user_00104 : (IN X (Set_Of A P)). Proof automatic_00104. End set_of_th1A. Lemma set_of_th1 : (A, X : Ens)(P : Ens -> Prop) ( Look_at ( Set_Of A P ) ) -> ( IN X A ) -> ( Apply1 P X ) -> ( IN X ( Set_Of A P ) ). Proof [A, X : Ens][P : Ens -> Prop][h : ( Look_at ( Set_Of A P ) )] [k : ( IN X A )] [l : ( P X )] (user_00104 A X P k l). Section set_of_th2A. Variables A,X: Ens. Variable P: Ens-> Prop. Hypothesis h : (IN X (Set_Of A P)). Remark user_00105 : (IN X ( REPLACEMENT ( Restriction P A ) )). Proof h. Remark user_00103 : (Consider1 (Restriction P A)). Proof (Just_consider1 (Restriction P A)). Remark automatic_00107 : (is_bounded ( Restriction P A ) ). Proof ( Restriction_bounded P A user_00103 ). Remark uautomatic_00109 : ( Restriction P A X ). Proof ( replacement_lem2 ( Restriction P A ) X automatic_00107 user_00105 ). OutRemark automatic_00112 : (IN X A ). Proof ( proj1_Restriction P A X uautomatic_00109 ). OutRemark automatic_00113 : (P X ). Proof ( proj2_Restriction P A X uautomatic_00109 ). End set_of_th2A. Lemma set_of_th2 : (A, X : Ens)(P : Ens -> Prop) ( IN X ( Set_Of A P ) ) -> ( IN X A ). Proof [A, X : Ens][P : Ens -> Prop][h : ( IN X ( Set_Of A P ) )] (automatic_00112 A X P h). Lemma set_of_th3 : (A, X : Ens)(P : Ens -> Prop) ( IN X ( Set_Of A P ) ) -> ( P X ). Proof [A, X : Ens][P : Ens -> Prop][h : ( IN X ( Set_Of A P ) )] (automatic_00113 A X P h). Section set_of_th4A. Variable A: Ens. Variable P: Ens-> Prop. Hypothesis l : (Look_at (Set_Of A P)). Section set_of_th4B. Variable X : Ens. Hypothesis h : (IN X (Set_Of A P)). OutRemark automatic_00115 : (IN X A ). Proof ( set_of_th2 A X P h ). End set_of_th4B. OutRemark autout_00116 : (SUB ( Set_Of A P ) A). Proof automatic_00115. End set_of_th4A. Lemma set_of_th4 : (A : Ens)(P : Ens -> Prop)( Look_at ( Set_Of A P ) ) -> ( SUB ( Set_Of A P ) A ). Proof [A : Ens][P : Ens -> Prop][l : ( Look_at ( Set_Of A P ) )] (autout_00116 A P). (****** intersection ********) Definition intersection := [A,B: Ens] (Set_Of A ([X_int: Ens] (IN X_int B))). Section intersection_th1A. Variables A,B: Ens. Hypothesis h: (Look_at (intersection A B)). Section intersection_th1B. Variable X: Ens. Hypothesis i: (IN X (intersection A B)). Remark user_00116 : (IN X (Set_Of A ([X_int: Ens] (IN X_int B)))). Proof i. OutRemark automatic_00118 : (IN X A ). Proof ( set_of_th2 A X ( [ X_int : Ens ] ( IN X_int B ) ) user_00116 ). OutRemark automatic_00119 : (IN X B ). Proof ( set_of_th3 A X ( [ X_int : Ens ] ( IN X_int B ) ) user_00116 ). End intersection_th1B. OutRemark autout_00120 : (SUB ( intersection A B ) A). Proof automatic_00118. OutRemark autout_00121 : (SUB ( intersection A B ) B). Proof automatic_00119. End intersection_th1A. Lemma intersection_th1 : (A, B : Ens)( Look_at ( intersection A B ) ) -> ( SUB ( intersection A B ) A ). Proof [A, B : Ens][h : ( Look_at ( intersection A B ) )] (autout_00120 A B). Lemma intersection_th2 : (A, B : Ens) ( Look_at ( intersection A B ) ) -> ( SUB ( intersection A B ) B ). Proof [A, B : Ens][h : ( Look_at ( intersection A B ) )] (autout_00121 A B). Section intersection_th3A. Variables A,B,X: Ens. Hypothesis h: (Look_at (intersection A B)). Hypothesis a : (IN X A). Hypothesis b: (IN X B). Remark user_00120 : (Look_at (Set_Of A ([X_int: Ens] (IN X_int B)))). Proof (Just_look_at (Set_Of A ([X_int: Ens] (IN X_int B)))). Remark user_00121 : (Apply1 ([X_int: Ens] (IN X_int B)) X). Proof b. OutRemark uautomatic_00124 : (IN X (intersection A B) ). Proof ( set_of_th1 A X ( [ X_int : Ens ] ( IN X_int B ) ) user_00120 a user_00121 ). End intersection_th3A. Lemma intersection_th3 : (A, B, X : Ens)( Look_at ( intersection A B ) ) -> ( IN X A ) -> ( IN X B ) -> ( IN X ( intersection A B ) ). Proof [A, B, X : Ens][h : ( Look_at ( intersection A B ) )] [a : ( IN X A )] [b : ( IN X B )] (uautomatic_00124 A B X a b). Section intersection_th4A. Variables A,B,C: Ens. Hypothesis h: (Look_at (intersection A B)). Hypothesis a: (SUB C A). Hypothesis b: (SUB C B). Section intersection_th4B. Variable X : Ens. Hypothesis i : (IN X C). Remark automatic_00120 : (IN X A ). Proof ( apply_SUB C A X a i ). Remark automatic_00121 : (IN X B ). Proof ( apply_SUB C B X b i ). OutRemark automatic_00128 : (IN X ( intersection A B ) ). Proof ( intersection_th3 A B X h automatic_00120 automatic_00121 ). End intersection_th4B. OutRemark autout_00129 : (SUB C ( intersection A B )). Proof automatic_00128. End intersection_th4A. Lemma intersection_th4 : (A, B, C : Ens)( Look_at ( intersection A B ) ) -> ( SUB C A ) -> ( SUB C B ) -> ( SUB C ( intersection A B ) ). Proof [A, B, C : Ens][h : ( Look_at ( intersection A B ) )] [a : ( SUB C A )] [b : ( SUB C B )] (autout_00129 A B C h a b). (**** Intersection *****) Property Intersection_prop := [K, X: Ens] (Y: Ens) (IN Y K ) -> (IN X Y). Lemma apply_Intersection_prop : (K, X, Y : Ens)( Intersection_prop K X ) -> ( IN Y K ) -> ( IN X Y ). Proof [K, X, Y : Ens][ hyp : ( Intersection_prop K X )] [ h00001 : ( IN Y K )] ( hyp Y h00001 ). Section Intersection_boundedA. Variable K : Ens. Hypothesis i : (is_nonempty K). Remark automatic_00136 : (IN ( Something_in K ) K ). Proof ( is_nonempty_th2 K i ). Section Intersection_boundedB. Variable X : Ens. Hypothesis x : (Apply1 (Intersection_prop K) X). Remark user_00137: (Intersection_prop K X). Proof x. OutRemark automatic_00138 : (IN X ( Something_in K ) ). Proof ( apply_Intersection_prop K X ( Something_in K ) user_00137 automatic_00136 ). End Intersection_boundedB. Remark autout_00139 : (bounds ( Intersection_prop K ) ( Something_in K )). Proof automatic_00138. OutRemark automatic_00139 : (is_bounded ( Intersection_prop K ) ). Proof ( bounded_th1 ( Intersection_prop K ) ( Something_in K ) autout_00139 ). End Intersection_boundedA. Lemma Intersection_bounded : (K : Ens)( is_nonempty K ) -> ( is_bounded ( Intersection_prop K ) ). Proof [K : Ens][i : ( is_nonempty K )] (automatic_00139 K i). Definition Intersection := [K: Ens] (REPLACEMENT (Intersection_prop K)). Section Intersection_th1A. Variables K,X,Y: Ens. Hypothesis x : (IN X K). Hypothesis y : (IN Y (Intersection K)). Remark user_00140 : (IN Y (REPLACEMENT (Intersection_prop K))). Proof y. Remark automatic_00140 : (is_nonempty K ). Proof ( is_nonempty_th1 K X x ). Remark automatic_00144 : (is_bounded ( Intersection_prop K ) ). Proof ( Intersection_bounded K automatic_00140 ). Remark automatic_00146 : ( Intersection_prop K Y ). Proof ( replacement_lem2 ( Intersection_prop K ) Y automatic_00144 user_00140 ). OutRemark automatic_00152 : (IN Y X ). Proof ( apply_Intersection_prop K Y X automatic_00146 x ). End Intersection_th1A. Lemma Intersection_th1 : (K, X, Y : Ens)( IN X K ) -> ( IN Y ( Intersection K ) ) -> ( IN Y X ). Proof [K, X, Y : Ens][x : ( IN X K )] [y : ( IN Y ( Intersection K ) )] (automatic_00152 K X Y x y). Section Intersection_th2A. Variables K,X : Ens. Hypothesis l : (Look_at (Intersection K)). Hypothesis x : (IN X K). Section Intersection_th2B. Variable Y: Ens. Hypothesis y : (IN Y (Intersection K)). OutRemark automatic_00155 : (IN Y X ). Proof ( Intersection_th1 K X Y x y ). End Intersection_th2B. OutRemark autout_00156 : (SUB ( Intersection K ) X). Proof automatic_00155. End Intersection_th2A. Lemma Intersection_th2 : (K, X : Ens)( Look_at ( Intersection K ) ) -> ( IN X K ) -> ( SUB ( Intersection K ) X ). Proof [K, X : Ens][l : ( Look_at ( Intersection K ) )] [x : ( IN X K )] (autout_00156 K X x). Section Intersection_th3A. Variables K,Y: Ens. Hypothesis k : (is_nonempty K). Hypothesis y : (Intersection_prop K Y). Remark automatic_00158 : (is_bounded ( Intersection_prop K ) ). Proof ( Intersection_bounded K k ). Remark user_00159 : (Apply1 (Intersection_prop K) Y). Proof y. OutRemark uautomatic_00162 : (IN Y (Intersection K) ). Proof ( replacement_lem1 ( Intersection_prop K ) Y automatic_00158 user_00159 ). End Intersection_th3A. Lemma Intersection_th3 : (K, Y : Ens)( is_nonempty K ) -> ( Intersection_prop K Y ) -> ( IN Y ( Intersection K ) ). Proof [K, Y : Ens][k : ( is_nonempty K )] [y : ( Intersection_prop K Y )] (uautomatic_00162 K Y k y). Property subsetIntersection := [K,A: Ens](X : Ens) (IN X K)-> (SUB A X). Lemma apply_subsetIntersection : (K, A, X : Ens)( subsetIntersection K A ) -> ( IN X K ) -> ( SUB A X ). Proof [K, A, X : Ens][ hyp : ( subsetIntersection K A )] [ h00001 : ( IN X K )] ( hyp X h00001 ). Section Intersection_th4A. Variables K,A: Ens. Hypothesis k : (is_nonempty K). Hypothesis a : (subsetIntersection K A). Section Intersection_th4B. Variable X : Ens. Hypothesis x : (IN X A). Section Intersection_th4C. Variable Y : Ens. Hypothesis y : (IN Y K). Remark automatic_00166 : (SUB A Y ). Proof ( apply_subsetIntersection K A Y a y ). OutRemark automatic_00167 : (IN X Y ). Proof ( apply_SUB A Y X automatic_00166 x ). End Intersection_th4C. Remark autout_00168 : (Intersection_prop K X). Proof automatic_00167. OutRemark automatic_00172 : (IN X ( Intersection K ) ). Proof ( Intersection_th3 K X k autout_00168 ). End Intersection_th4B. OutRemark autout_00173 : (SUB A ( Intersection K )). Proof automatic_00172. End Intersection_th4A. Lemma Intersection_th4 : (K, A : Ens)( is_nonempty K ) -> ( subsetIntersection K A ) -> ( SUB A ( Intersection K ) ). Proof [K, A : Ens][k : ( is_nonempty K )] [a : ( subsetIntersection K A )] (autout_00173 K A k a). (********* extensionality ******************) Axiom substitute : (A,B: Ens) (P: Ens-> Prop) (EQ A B) -> (P B) -> (P A). Section Substitute11A. Variable A: Ens. Variable P: Ens-> Prop. Variable B: Ens. Hypothesis e : (EQ A B). Hypothesis p : (Apply1 P B). OutRemark subst11out : (Apply1 P A). Proof (substitute A B P e p). End Substitute11A. Lemma Substitute11 : (A : Ens)(P : Ens -> Prop) (B : Ens)( EQ A B ) -> ( Apply1 P B ) -> ( Apply1 P A ). Proof [A : Ens][P : Ens -> Prop][B : Ens][e : ( EQ A B )] [p : ( Apply1 P B )] (subst11out A P B e p). Section Substitute12A. Variable X: Ens. Variable P: Ens-> Ens-> Prop. Variables A,B: Ens. Hypothesis p : (Apply2 P A B). Hypothesis e : (EQ X A). Remark subs12a : (Apply1 ([W: Ens] (P W B)) A). Proof p. OutRemark automatic_00178 : (Apply2 P X B ). Proof ( Substitute11 X ( [ W : Ens ] ( P W B ) ) A e subs12a ). End Substitute12A. Lemma Substitute12 : (X : Ens)(P : Ens -> Ens -> Prop) (A, B : Ens)( Apply2 P A B ) -> ( EQ X A ) -> ( Apply2 P X B ). Proof [X : Ens][P : Ens -> Ens -> Prop][A, B : Ens][p : ( Apply2 P A B )] [e : ( EQ X A )] (automatic_00178 X P A B p e). Section Substitute22A. Variable X: Ens. Variable P: Ens -> Ens -> Prop. Variables A,B: Ens. Hypothesis p : (Apply2 P A B). Hypothesis e : (EQ X B). Remark subs12a : (Apply1 ([W: Ens] (P A W)) B). Proof p. OutRemark automatic_00183 : (Apply2 P A X ). Proof ( Substitute11 X ( [ W : Ens ] ( P A W ) ) B e subs12a ). End Substitute22A. Lemma Substitute22 : (X : Ens)(P : Ens -> Ens -> Prop)(A, B : Ens) ( Apply2 P A B ) -> ( EQ X B ) -> ( Apply2 P A X ). Proof [X : Ens][P : Ens -> Ens -> Prop][A, B : Ens][p : ( Apply2 P A B )] [e : ( EQ X B )] (automatic_00183 X P A B p e). Section Substitute13A. Variable X: Ens. Variable P: Ens -> Ens -> Ens -> Prop. Variables A,B,C: Ens. Hypothesis p : (Apply3 P A B C). Hypothesis e : (EQ X A). Remark subs12a : (Apply1 ([W: Ens] (P W B C)) A). Proof p. OutRemark automatic_00188 : (Apply3 P X B C ). Proof ( Substitute11 X ( [ W : Ens ] ( P W B C ) ) A e subs12a ). End Substitute13A. Lemma Substitute13 : (X : Ens)(P : Ens -> Ens -> Ens -> Prop)(A, B, C : Ens) ( Apply3 P A B C ) -> ( EQ X A ) -> ( Apply3 P X B C ). Proof [X : Ens][P : Ens -> Ens -> Ens -> Prop][A, B, C : Ens][p : ( Apply3 P A B C )] [e : ( EQ X A )] (automatic_00188 X P A B C p e). Section Substitute23A. Variable X: Ens. Variable P: Ens -> Ens -> Ens-> Prop. Variables A,B,C: Ens. Hypothesis p : (Apply3 P A B C). Hypothesis e : (EQ X B). Remark subs12a : (Apply1 ([W: Ens] (P A W C)) B). Proof p. OutRemark automatic_00193 : (Apply3 P A X C ). Proof ( Substitute11 X ( [ W : Ens ] ( P A W C ) ) B e subs12a ). End Substitute23A. Lemma Substitute23 : (X : Ens)(P : Ens -> Ens -> Ens -> Prop)(A, B, C : Ens) ( Apply3 P A B C ) -> ( EQ X B ) -> ( Apply3 P A X C ). Proof [X : Ens][P : Ens -> Ens -> Ens -> Prop][A, B, C : Ens][p : ( Apply3 P A B C )] [e : ( EQ X B )] (automatic_00193 X P A B C p e). Section Substitute33A. Variable X: Ens. Variable P: Ens -> Ens -> Ens-> Prop. Variables A,B,C: Ens. Hypothesis p : (Apply3 P A B C). Hypothesis e : (EQ X C). Remark subs12a : (Apply1 ([W: Ens] (P A B W)) C). Proof p. OutRemark automatic_00198 : (Apply3 P A B X ). Proof ( Substitute11 X ( [ W : Ens ] ( P A B W ) ) C e subs12a ). End Substitute33A. Lemma Substitute33 : (X : Ens)(P : Ens -> Ens -> Ens -> Prop)(A, B, C : Ens) ( Apply3 P A B C ) -> ( EQ X C ) -> ( Apply3 P A B X ). Proof [X : Ens][P : Ens -> Ens -> Ens -> Prop][A, B, C : Ens][p : ( Apply3 P A B C )] [e : ( EQ X C )] (automatic_00198 X P A B C p e). (****** Singletons *******) Section Singleton_th1A. Variables X,A: Ens. Hypothesis i : (IN X A). Hypothesis l : (Look_at (Singleton X)). Section Singleton_th1Aa. Variable Z : Ens. Hypothesis z : (IN Z (Singleton X)). Remark automatic_00200 : (EQ X Z ). Proof ( Singleton_lem2 X Z z ). Remark user_00201 : (Apply2 IN X A). Proof i. Remark automatic_00204 : (EQ Z X ). Proof ( EQ_symm X Z automatic_00200 ). OutRemark uautomatic_00215 : (IN Z A ). Proof ( Substitute12 Z IN X A user_00201 automatic_00204 ). End Singleton_th1Aa. OutRemark autout_00216 : (SUB ( Singleton X ) A). Proof uautomatic_00215. End Singleton_th1A. Lemma Singleton_th1 : (X, A : Ens)( IN X A ) -> ( Look_at ( Singleton X ) ) -> ( SUB ( Singleton X ) A ). Proof [X, A : Ens][i : ( IN X A )] [l : ( Look_at ( Singleton X ) )] (autout_00216 X A i). Section Singleton_th2A. Variable X: Ens. Hypothesis l : (Look_at (Singleton X)). Remark automatic_00217 : (IN X ( Singleton X ) ). Proof ( Singleton_lem1 X l ). OutRemark automatic_00220 : (is_nonempty ( Singleton X ) ). Proof ( is_nonempty_th1 ( Singleton X ) X automatic_00217 ). End Singleton_th2A. Lemma Singleton_th2 : (X : Ens)( Look_at ( Singleton X ) ) -> ( is_nonempty ( Singleton X ) ). Proof [X : Ens][l : ( Look_at ( Singleton X ) )] (automatic_00220 X l). (****** more on union ****) Section union_th1A. Variables A,B,X: Ens. Hypothesis h : (IN X (union A B)). Remark user_00222 : (Look_at (union A B)). Proof (Just_look_at (union A B)). Remark automatic_00248 : (SUB A ( union A B ) ). Proof ( union_lem1 A B user_00222 ). Remark automatic_00249 : (SUB B ( union A B ) ). Proof ( union_lem2 A B user_00222 ). Remark user_00240 : (Consider0 (OR (IN X A) (IN X B))). Proof (Just_consider0 (OR (IN X A) (IN X B))). Section union_th1B. Hypothesis n : (NOT (OR (IN X A) (IN X B))). Local W:= (Set_Of (union A B) ([Z: Ens] (NEQ Z X))). Remark user_00221: (Look_at (Set_Of (union A B) ([Z: Ens] (NEQ Z X)))). Proof (Just_look_at (Set_Of (union A B) ([Z: Ens] (NEQ Z X)))). Remark automatic_00224 : (SUB W ( union A B ) ). Proof ( set_of_th4 ( union A B ) ( [ Z : Ens ] ( NEQ Z X ) ) user_00221 ). Section union_th1C. Variable Y: Ens. Hypothesis ya : (IN Y A). Section union_th1D. Hypothesis yan : (EQ Y X). Remark user_00225 : (Apply2 IN Y A). Proof ya. Remark automatic_00228 : (EQ X Y ). Proof ( EQ_symm Y X yan ). Remark automatic_00239 : (Apply0 (IN X A )). Proof ( Substitute12 X IN Y A user_00225 automatic_00228 ). Remark automatic_00241 : (Apply0 (OR ( IN X A ) ( IN X B ) )). Proof ( OR_lem1 ( IN X A ) ( IN X B ) user_00240 automatic_00239 ). OutRemark automatic_00243 : FALSE . Proof ( apply_NOT ( OR ( IN X A ) ( IN X B ) ) n automatic_00241 ). End union_th1D. Remark autout_00245 : (NEQ Y X). Proof automatic_00243. Remark user_00246 : (Apply1 ([Z: Ens] (NEQ Z X)) Y). Proof autout_00245. Remark automatic_00250 : (IN Y ( union A B ) ). Proof ( apply_SUB A ( union A B ) Y automatic_00248 ya ). OutRemark automatic_00259 : (IN Y W ). Proof ( set_of_th1 ( union A B ) Y ( [ Z : Ens ] ( NEQ Z X ) ) user_00221 automatic_00250 user_00246 ). End union_th1C. Remark autout_00260 : (SUB A W). Proof automatic_00259. Section union_th1E. Variable Y: Ens. Hypothesis yb : (IN Y B). Remark automatic_00262 : (IN Y ( union A B ) ). Proof ( apply_SUB B ( union A B ) Y automatic_00249 yb ). Section union_th1F. Hypothesis ybn : (EQ Y X). Remark user_00261 : (Apply2 IN Y B). Proof yb. Remark automatic_00265 : (EQ X Y ). Proof ( EQ_symm Y X ybn ). Remark automatic_00279 : (Apply0 (IN X B) ). Proof ( Substitute12 X IN Y B user_00261 automatic_00265 ). Remark automatic_00280 : (Apply0 (OR ( IN X A ) ( IN X B ) )). Proof ( OR_lem2 ( IN X A ) ( IN X B ) user_00240 automatic_00279 ). OutRemark automatic_00282 : FALSE . Proof ( apply_NOT ( OR ( IN X A ) ( IN X B ) ) n automatic_00280 ). End union_th1F. Remark autout_00284 : (NEQ Y X). Proof automatic_00282. Remark user_00285 : (Apply1 ([Z: Ens] (NEQ Z X)) Y). Proof autout_00284. OutRemark automatic_00294 : (IN Y W ). Proof ( set_of_th1 ( union A B ) Y ( [ Z : Ens ] ( NEQ Z X ) ) user_00221 automatic_00262 user_00285 ). End union_th1E. Remark autout_00295 : (SUB B W). Proof automatic_00294. Remark automatic_00297 : (SUB ( union A B ) W ). Proof ( union_lem3 A B W autout_00260 autout_00295 user_00222 ). Remark automatic_00298 : (IN X W ). Proof ( apply_SUB ( union A B ) W X automatic_00297 h ). Remark user_00299 : (IN X (Set_Of (union A B) ([Z: Ens] (NEQ Z X)))). Proof automatic_00298. Remark uautomatic_00310 : (NEQ X X ). Proof ( set_of_th3 ( union A B ) X ( [ Z : Ens ] ( NEQ Z X ) ) user_00299 ). Remark user_00311 : (EQ X X). Proof (EQ_refl X). OutRemark automatic_00324 : FALSE . Proof ( apply_NEQ X X uautomatic_00310 user_00311 ). End union_th1B. Remark autout_00325 : (NOT ( NOT ( OR ( IN X A ) ( IN X B ) ) )). Proof automatic_00324. OutRemark automatic_00326 : ( OR ( IN X A ) ( IN X B ) ) . Proof ( excluded_middle ( OR ( IN X A ) ( IN X B ) ) autout_00325 ). End union_th1A. Lemma union_th1 : (A, B, X : Ens)( IN X ( union A B ) ) -> ( OR ( IN X A ) ( IN X B ) ). Proof [A, B, X : Ens][h : ( IN X ( union A B ) )] (automatic_00326 A B X h). Section union_reflA. Variable A: Ens. Hypothesis l: (Look_at (union A A)). Remark automatic_00327 : (SUB A ( union A A ) ). Proof ( union_lem1 A A l ). Remark user_00328: (SUB A A). Proof (SUB_refl A). Remark automatic_00331 : (SUB ( union A A ) A ). Proof ( union_lem3 A A A user_00328 user_00328 l ). OutRemark automatic_00333 : (EQ A ( union A A ) ). Proof ( conj_EQ A ( union A A ) automatic_00327 automatic_00331 ). End union_reflA. Lemma union_refl : (A : Ens)( Look_at ( union A A ) ) -> ( EQ A ( union A A ) ). Proof [A : Ens][l : ( Look_at ( union A A ) )] (automatic_00333 A l). Section union_symmA. Variables A,B: Ens. Hypothesis l : (Look_at (union A B)). Hypothesis m : (Look_at (union B A)). Remark automatic_00334 : (SUB A ( union A B ) ). Proof ( union_lem1 A B l ). Remark automatic_00335 : (SUB B ( union B A ) ). Proof ( union_lem1 B A m ). Remark automatic_00336 : (SUB B ( union A B ) ). Proof ( union_lem2 A B l ). Remark automatic_00337 : (SUB A ( union B A ) ). Proof ( union_lem2 B A m ). Remark automatic_00339 : (SUB ( union A B ) ( union B A ) ). Proof ( union_lem3 A B ( union B A ) automatic_00337 automatic_00335 l ). Remark automatic_00340 : (SUB ( union B A ) ( union A B ) ). Proof ( union_lem3 B A ( union A B ) automatic_00336 automatic_00334 m ). OutRemark automatic_00341 : (EQ ( union A B ) ( union B A ) ). Proof ( conj_EQ ( union A B ) ( union B A ) automatic_00339 automatic_00340 ). End union_symmA. Lemma union_symm : (A, B : Ens)( Look_at ( union A B ) ) -> ( Look_at ( union B A ) ) -> ( EQ ( union A B ) ( union B A ) ). Proof [A, B : Ens][l : ( Look_at ( union A B ) )] [m : ( Look_at ( union B A ) )] (automatic_00341 A B l m).