set N = { x where x is Element of Q : f . x = 1. Q2 } ;
{ x where x is Element of Q : f . x = 1. Q2 } c= the carrier of Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of Q : f . x = 1. Q2 } or x in the carrier of Q )
assume x in { x where x is Element of Q : f . x = 1. Q2 } ; :: thesis: x in the carrier of Q
then ex x1 being Element of Q st
( x = x1 & f . x1 = 1. Q2 ) ;
hence x in the carrier of Q ; :: thesis: verum

end;

then reconsider N = { x where x is Element of Q : f . x = 1. Q2 } as Subset of Q ;
take N ; :: thesis: for x being Element of Q holds
( x in N iff f . x = 1. Q2 )
for x being Element of Q st x in N holds
f . x = 1. Q2

proof

let x be Element of Q; :: thesis: ( x in N implies f . x = 1. Q2 )
assume x in N ; :: thesis: f . x = 1. Q2
then ex x1 being Element of Q st
( x = x1 & f . x1 = 1. Q2 ) ;
hence f . x = 1. Q2 ; :: thesis: verum

end;

hence for x being Element of Q holds
( x in N iff f . x = 1. Q2 ) ; :: thesis: verum