let FT be non empty RelStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 )

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; :: thesis: 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; :: thesis: ( 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 )

proof

( ex y1 being Element of FT st P_1 (x,y1,A) = TRUE implies x in A ^b )
reconsider z = x as Element of FT ;

assume x in A ^b ; :: thesis: ex y1 being Element of FT st P_1 (x,y1,A) = TRUE

then U_FT z meets A by FIN_TOPO:8;

then consider w being object such that

A2: w in U_FT z and

A3: w in A by XBOOLE_0:3;

reconsider w = w as Element of FT 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;assume x in A ^b ; :: thesis: ex y1 being Element of FT st P_1 (x,y1,A) = TRUE

then U_FT z meets A by FIN_TOPO:8;

then consider w being object such that

A2: w in U_FT z and

A3: w in A by XBOOLE_0:3;

reconsider w = w as Element of FT by A2;

take w ; :: thesis: P_1 (x,w,A) = TRUE

thus P_1 (x,w,A) = TRUE by A2, A3, Def1; :: thesis: verum

proof

hence
( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE )
by A1; :: thesis: verum
given y being Element of FT 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 ;

hence x in A ^b ; :: thesis: verum

end;( 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 ;

hence x in A ^b ; :: thesis: verum