let R be Relation; :: thesis: for X being set st X has_upper_Zorn_property_wrt R holds
X <> {}
let X be set ; :: thesis: ( X has_upper_Zorn_property_wrt R implies X <> {} )
assume A1: for Y being set st Y c= X & R |_2 Y is being_linear-order holds
ex x being set st
( x in X & ( for y being set st y in Y holds
[y,x] in R ) ) ; :: according to ORDERS_1:def 9 :: thesis: X <> {}
( {} c= X & R |_2 {} is being_linear-order ) by Lm16, Th119, XBOOLE_1:2;
then ex x being set st
( x in X & ( for y being set st y in {} holds
[y,x] in R ) ) by A1;
hence X <> {} ; :: thesis: verum