let T be non empty RelStr ; :: thesis: for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
let x be Element of T; :: thesis: for A being upper Subset of T st not x in A holds
A misses downarrow x
let A be upper Subset of T; :: thesis: ( not x in A implies A misses downarrow x )
assume A1: not x in A ; :: thesis: A misses downarrow x
assume A meets downarrow x ; :: thesis: contradiction
then consider y being object such that
A2: y in A and
A3: y in downarrow x by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
y <= x by A3, WAYBEL_0:17;
hence contradiction by A1, A2, WAYBEL_0:def 20; :: thesis: verum