let T be non empty RelStr ; :: thesis: for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
let x be Element of T; :: thesis: for A being lower Subset of T st x in A holds
downarrow x c= A
let A be lower Subset of T; :: thesis: ( x in A implies downarrow x c= A )
assume x in A ; :: thesis: downarrow x c= A
then not x in A ` by XBOOLE_0:def 5;
then A ` misses downarrow x by Th5;
then A ` c= (downarrow x) ` by SUBSET_1:23;
hence downarrow x c= A by SUBSET_1:12; :: thesis: verum