Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove (∀x : set, x ∈ X → x ∈ path_component_of X Tx x) ∧ (∀x y : set, x ∈ X → y ∈ X → y ∈ path_component_of X Tx x → x ∈ path_component_of X Tx y) ∧ (∀x y z : set, x ∈ X → y ∈ X → z ∈ X → y ∈ path_component_of X Tx x → z ∈ path_component_of X Tx y → z ∈ path_component_of X Tx x).
Apply andI to the current goal.
Apply andI to the current goal.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (path_component_reflexive X Tx x HTx HxX).
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HyPc: y ∈ path_component_of X Tx x.
An exact proof term for the current goal is (path_component_symmetric_axiom X Tx x y HTx HxX HyX HyPc).
Let x, y and z be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume HzX: z ∈ X.
Assume HyPc: y ∈ path_component_of X Tx x.
Assume HzPc: z ∈ path_component_of X Tx y.
An exact proof term for the current goal is (path_component_transitive_axiom X Tx x y z HTx HxX HyX HzX HyPc HzPc).
∎