let N be non empty reflexive RelStr ; :: thesis: for x being Element of N
for X being Subset of N st x in X holds
downarrow x c= downarrow X
let x be Element of N; :: thesis: for X being Subset of N st x in X holds
downarrow x c= downarrow X
let X be Subset of N; :: thesis: ( x in X implies downarrow x c= downarrow X )
assume A1: x in X ; :: thesis: downarrow x c= downarrow X
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in downarrow x or a in downarrow X )
assume A2: a in downarrow x ; :: thesis: a in downarrow X
then reconsider b = a as Element of N ;
b <= x by A2, WAYBEL_0:17;
hence a in downarrow X by A1, WAYBEL_0:def 15; :: thesis: verum