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

for A being Subset of FT holds

( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

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

( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

let A be Subset of FT; :: thesis: ( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

thus ( x in A ^s implies ( x in A & (U_FT x) \ {x} misses A ) ) :: thesis: ( x in A & (U_FT x) \ {x} misses A implies x in A ^s )

hence x in A ^s ; :: thesis: verum

for A being Subset of FT holds

( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

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

( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

let A be Subset of FT; :: thesis: ( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )

thus ( x in A ^s implies ( x in A & (U_FT x) \ {x} misses A ) ) :: thesis: ( x in A & (U_FT x) \ {x} misses A implies x in A ^s )

proof

assume
( x in A & (U_FT x) \ {x} misses A )
; :: thesis: x in A ^s
assume
x in A ^s
; :: thesis: ( x in A & (U_FT x) \ {x} misses A )

then ex y being Element of FT st

( y = x & y in A & (U_FT y) \ {y} misses A ) ;

hence ( x in A & (U_FT x) \ {x} misses A ) ; :: thesis: verum

end;then ex y being Element of FT st

( y = x & y in A & (U_FT y) \ {y} misses A ) ;

hence ( x in A & (U_FT x) \ {x} misses A ) ; :: thesis: verum

hence x in A ^s ; :: thesis: verum