let A be non empty Poset; :: thesis: for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S
let a be Element of A; :: thesis: for S being Subset of A st a in S holds
not a in LowerCone S
let S be Subset of A; :: thesis: ( a in S implies not a in LowerCone S )
assume that
A1: a in S and
A2: a in LowerCone S ; :: thesis: contradiction
ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a1 < a2 ) ) by A2;
hence contradiction by A1; :: thesis: verum