let A, B be Subset of (TOP-REAL F₁()); :: thesis: ( ( for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] ) ) & ( for p being Point of (TOP-REAL F₁()) holds
( p in B iff P₁[p] ) ) implies A = B )
assume that
A1: for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] ) and
A2: for p being Point of (TOP-REAL F₁()) holds
( p in B iff P₁[p] ) ; :: thesis: A = B
thus for x being object st x in A holds
x in B by A2, A1; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume A3: x in B ; :: thesis: x in A
then P₁[x] by A2;
hence x in A by A1, A3; :: thesis: verum