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 )

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

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

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

( x in A ^deltao implies ( ex y1, y2 being Element of FT st
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;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

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

proof

hence
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
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;( 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

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