let D1, D2 be Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):]; :: thesis: ( D1 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
D1 c= D ) & D2 is_Sep-closed_on p & ( for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
D2 c= D ) implies D1 = D2 )
assume that
A17: D1 is_Sep-closed_on p and
A18: for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
D1 c= D and
A19: D2 is_Sep-closed_on p and
A20: for D being Subset of [:CQC-WFF ,NAT ,(Fin bound_QC-variables ),(Funcs bound_QC-variables ,bound_QC-variables ):] st D is_Sep-closed_on p holds
D2 c= D ; :: thesis: D1 = D2
thus ( D1 c= D2 & D2 c= D1 ) by A17, A18, A19, A20; :: according to XBOOLE_0:def 10 :: thesis: verum