let D1, D2 be Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):]; :: thesis: ( D1 is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] st D is_Sep-closed_on p holds
D1 c= D ) & D2 is_Sep-closed_on p & ( for D being Subset of [:(CQC-WFF A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] 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 A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] 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 A),(QC-symbols A),(Fin (bound_QC-variables A)),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):] 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