let FT be non empty RelStr ; :: thesis: for x being Element of FT

for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

let A be Subset of FT; :: thesis: ( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

A1: ( x in A ^delta implies ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) implies x in A ^delta )

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) by A1; :: thesis: verum

for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

let x be Element of FT; :: thesis: for A being Subset of FT holds

( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

let A be Subset of FT; :: thesis: ( x in A ^delta iff ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

A1: ( x in A ^delta implies ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) )

proof

( ex y1, y2 being Element of FT st
reconsider z = x as Element of FT ;

assume A2: x in A ^delta ; :: thesis: ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE )

then U_FT z meets A by FIN_TOPO:5;

then consider w1 being object such that

A3: w1 in U_FT z and

A4: w1 in A by XBOOLE_0:3;

reconsider w1 = w1 as Element of FT by A3;

take w1 ; :: thesis: ex y2 being Element of FT st

( P_1 (x,w1,A) = TRUE & P_2 (x,y2,A) = TRUE )

U_FT z meets A ` by A2, FIN_TOPO:5;

then consider w2 being object such that

A5: ( w2 in U_FT z & w2 in A ` ) by XBOOLE_0:3;

take w2 ; :: thesis: ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE )

thus ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) by A3, A4, A5, Def1, Def2; :: thesis: verum

end;assume A2: x in A ^delta ; :: thesis: ex y1, y2 being Element of FT st

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE )

then U_FT z meets A by FIN_TOPO:5;

then consider w1 being object such that

A3: w1 in U_FT z and

A4: w1 in A by XBOOLE_0:3;

reconsider w1 = w1 as Element of FT by A3;

take w1 ; :: thesis: ex y2 being Element of FT st

( P_1 (x,w1,A) = TRUE & P_2 (x,y2,A) = TRUE )

U_FT z meets A ` by A2, FIN_TOPO:5;

then consider w2 being object such that

A5: ( w2 in U_FT z & w2 in A ` ) by XBOOLE_0:3;

take w2 ; :: thesis: ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE )

thus ( w2 is set & w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) by A3, A4, A5, Def1, Def2; :: thesis: verum

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) implies x in A ^delta )

proof

hence
( x in A ^delta iff ex y1, y2 being Element of FT st
given y1, y2 being Element of FT such that A6:
P_1 (x,y1,A) = TRUE
and

A7: P_2 (x,y2,A) = TRUE ; :: thesis: x in A ^delta

( y1 in U_FT x & y1 in A ) by A6, Def1;

then (U_FT x) /\ A <> {} by XBOOLE_0:def 4;

then A8: U_FT x meets A ;

( y2 in U_FT x & y2 in A ` ) by A7, Def2;

then U_FT x meets A ` by XBOOLE_0:3;

hence x in A ^delta by A8; :: thesis: verum

end;A7: P_2 (x,y2,A) = TRUE ; :: thesis: x in A ^delta

( y1 in U_FT x & y1 in A ) by A6, Def1;

then (U_FT x) /\ A <> {} by XBOOLE_0:def 4;

then A8: U_FT x meets A ;

( y2 in U_FT x & y2 in A ` ) by A7, Def2;

then U_FT x meets A ` by XBOOLE_0:3;

hence x in A ^delta by A8; :: thesis: verum

( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) by A1; :: thesis: verum