let FT be non empty RelStr ; for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
let x be Element of FT; for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
let A be Subset of FT; ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
A1:
( x in A ^b implies ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
( ex y1 being Element of FT st P_1 (x,y1,A) = TRUE implies x in A ^b )
hence
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
by A1; verum