let T be non empty RelStr ; :: thesis: for A being Subset of T
for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
let A be Subset of T; :: thesis: for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
let x be Element of T; :: thesis: ( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
thus ( x in A ^d implies for y being Element of T st y in A ` holds
not x in U_FT y ) :: thesis: ( ( for y being Element of T st y in A ` holds
not x in U_FT y ) implies x in A ^d )

proof

assume x in A ^d ; :: thesis: for y being Element of T st y in A ` holds
not x in U_FT y
then ex y being Element of T st
( y = x & ( for z being Element of T st z in A ` holds
not y in U_FT z ) ) ;
hence for y being Element of T st y in A ` holds
not x in U_FT y ; :: thesis: verum

end;

assume for z being Element of T st z in A ` holds
not x in U_FT z ; :: thesis: x in A ^d
hence x in A ^d ; :: thesis: verum