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 <> {}
R |_2 {} is being_linear-order by Lm16, Th119;
then ex x being set st
( x in X & ( for y being set st y in {} holds
[y,x] in R ) ) by A1, XBOOLE_1:2;
hence X <> {} ; :: thesis: verum