let L be antisymmetric RelStr ; :: thesis: for X being set holds
( ex_inf_of X,L iff ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) ) )
let X be set ; :: thesis: ( ex_inf_of X,L iff ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) ) )

hereby :: thesis: ( ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) ) implies ex_inf_of X,L )

assume ex_inf_of X,L ; :: thesis: ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) )
then ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a ) ) by Def8;
hence ex a being Element of L st
( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) ) ; :: thesis: verum

end;

given a being Element of L such that A1: X is_>=_than a and
A2: for b being Element of L st X is_>=_than b holds
a >= b ; :: thesis: ex_inf_of X,L
take a ; :: according to YELLOW_0:def 8 :: thesis: ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
b <= a ) & ( for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a ) )
thus ( X is_>=_than a & ( for b being Element of L st X is_>=_than b holds
a >= b ) ) by A1, A2; :: thesis: for c being Element of L st X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) holds
c = a
let c be Element of L; :: thesis: ( X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
b <= c ) implies c = a )
assume ( X is_>=_than c & ( for b being Element of L st X is_>=_than b holds
c >= b ) ) ; :: thesis: c = a
then ( a <= c & c <= a ) by A1, A2;
hence c = a by ORDERS_2:25; :: thesis: verum