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