let D be set ; :: thesis: for F, G being Subset-Family of D st ( for P being Subset of D holds

( P in F iff P in G ) ) holds

F = G

let F, G be Subset-Family of D; :: thesis: ( ( for P being Subset of D holds

( P in F iff P in G ) ) implies F = G )

assume A1: for P being Subset of D holds

( P in F iff P in G ) ; :: thesis: F = G

thus F c= G by A1; :: according to XBOOLE_0:def 10 :: thesis: G c= F

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in F )

assume x in G ; :: thesis: x in F

hence x in F by A1; :: thesis: verum

( P in F iff P in G ) ) holds

F = G

let F, G be Subset-Family of D; :: thesis: ( ( for P being Subset of D holds

( P in F iff P in G ) ) implies F = G )

assume A1: for P being Subset of D holds

( P in F iff P in G ) ; :: thesis: F = G

thus F c= G by A1; :: according to XBOOLE_0:def 10 :: thesis: G c= F

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G or x in F )

assume x in G ; :: thesis: x in F

hence x in F by A1; :: thesis: verum