let C1, C2 be Subset-Family of Q; :: thesis: ( ( for H being Subset of Q holds
( H in C1 iff ex x being Element of Q st H = x * N ) ) & ( for H being Subset of Q holds
( H in C2 iff ex x being Element of Q st H = x * N ) ) implies C1 = C2 )
assume that
A1: for H being Subset of Q holds
( H in C1 iff ex x being Element of Q st H = x * N ) and
A2: for H being Subset of Q holds
( H in C2 iff ex x being Element of Q st H = x * N ) ; :: thesis: C1 = C2
thus C1 c= C2 :: according to XBOOLE_0:def 10 :: thesis: C2 c= C1

proof

let H be object ; :: according to TARSKI:def 3 :: thesis: ( not H in C1 or H in C2 )
reconsider H1 = H as set by TARSKI:1;
assume H in C1 ; :: thesis: H in C2
then ex x being Element of Q st H = x * N by A1;
hence H in C2 by A2; :: thesis: verum

end;

let H be object ; :: according to TARSKI:def 3 :: thesis: ( not H in C2 or H in C1 )
reconsider H1 = H as set by TARSKI:1;
assume H in C2 ; :: thesis: H in C1
then ex x being Element of Q st H = x * N by A2;
hence H in C1 by A1; :: thesis: verum