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

proof

assume that
A2: ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) and
A3: P_A (x,A) = FALSE ; :: thesis: x in A ^deltao
not x in A by A3, Def4;
then A4: x in A ` by XBOOLE_0:def 5;
x in A ^delta by A2, Th8;
hence x in A ^deltao by A4, XBOOLE_0:def 4; :: thesis: verum

end;

( x in A ^deltao implies ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) )

proof

assume A5: x in A ^deltao ; :: thesis: ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE )
then x in A ` by XBOOLE_0:def 4;
then A6: not x in A by XBOOLE_0:def 5;
x in A ^delta by A5, XBOOLE_0:def 4;
hence ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) by A6, Def4, Th8; :: thesis: verum

end;

hence ( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) by A1; :: thesis: verum