let L1 be non empty Poset; :: thesis: for A being Subset of L1
for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
let A be Subset of L1; :: thesis: for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}
let a be Element of L1; :: thesis: ( a in uparrow A implies Way_Up (a,A) = {} )
assume A1: a in uparrow A ; :: thesis: Way_Up (a,A) = {}
wayabove a c= uparrow A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in wayabove a or z in uparrow A )
assume A2: z in wayabove a ; :: thesis: z in uparrow A
then reconsider z1 = z as Element of L1 ;
a << z1 by A2, WAYBEL_3:8;
then a <= z1 by WAYBEL_3:1;
hence z in uparrow A by A1, WAYBEL_0:def 20; :: thesis: verum

end;

hence Way_Up (a,A) = {} by XBOOLE_1:37; :: thesis: verum