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 UpperCone S
let a be Element of A; :: thesis: for S being Subset of A st a in S holds
not a in UpperCone S
let S be Subset of A; :: thesis: ( a in S implies not a in UpperCone S )
assume that
A1: a in S and
A2: a in UpperCone S ; :: thesis: contradiction
ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) by A2;
hence contradiction by A1; :: thesis: verum