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

proof

reconsider z = x as Element of ;
assume x in A ^b ; :: thesis: ex y1 being Element of st P_1 x,y1,A = TRUE
then U_FT z meets A by FIN_TOPO:13;
then consider w being set such that
A2: w in U_FT z and
A3: w in A by XBOOLE_0:3;
reconsider w = w as Element of by A2;
take w ; :: thesis: P_1 x,w,A = TRUE
thus P_1 x,w,A = TRUE by A2, A3, Def1; :: thesis: verum

end;

( ex y1 being Element of st P_1 x,y1,A = TRUE implies x in A ^b )

proof

given y being Element of such that A4: P_1 x,y,A = TRUE ; :: thesis: x in A ^b
( y in U_FT x & y in A ) by A4, Def1;
then y in (U_FT x) /\ A by XBOOLE_0:def 4;
then U_FT x meets A by XBOOLE_0:def 7;
hence x in A ^b ; :: thesis: verum

end;

hence ( x in A ^b iff ex y1 being Element of st P_1 x,y1,A = TRUE ) by A1; :: thesis: verum