# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677991317 -32400
# Node ID 93e1869bb57ca3c7d3fc485eb05b8387698af4c7
# Parent  22de2d4f72717721e8e1e9efd5dbb41e52192842
...

diff -r 22de2d4f7271 -r 93e1869bb57c src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Mar 05 12:16:07 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 13:41:57 2023 +0900
@@ -359,7 +359,13 @@
                   ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
                        (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 ))  )
                   x⊆pxq : * x ⊆ ZFP p Q
-                  x⊆pxq = ?
+                  x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
+                  ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
+                      ty07 : odef (* x) (& < * a , * b >) 
+                      ty07 = xw
+                      ty08 : odef p a
+                      ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))  
+                           record { z = _ ; az = xw ;  x=ψz = ? }
                   ty05 : filter F ∋  ZFP p Q
                   ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq
                   ty06 : ZFP p Q ⊆ ZFP q Q