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
uparrow x c= uparrow X
let x be Element of N; :: thesis: for X being Subset of N st x in X holds
uparrow x c= uparrow X
let X be Subset of N; :: thesis: ( x in X implies uparrow x c= uparrow X )
assume A1: x in X ; :: thesis: uparrow x c= uparrow X
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in uparrow x or a in uparrow X )
assume A2: a in uparrow x ; :: thesis: a in uparrow X
then reconsider b = a as Element of N ;
x <= b by A2, WAYBEL_0:18;
hence a in uparrow X by A1, WAYBEL_0:def 16; :: thesis: verum