let FT be non empty RelStr ; :: thesis: for x being Element of
for A being Subset of holds
( x in A ^deltao iff ( ex y1, y2 being Element of st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) )
let x be Element of ; :: thesis: for A being Subset of holds
( x in A ^deltao iff ( ex y1, y2 being Element of st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) )
let A be Subset of ; :: thesis: ( x in A ^deltao iff ( ex y1, y2 being Element of 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 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 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 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 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 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 st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) ) by A1; :: thesis: verum