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 ) ) )
thus ( ex_inf_of X,L implies 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: ( 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 )
given a being Element of L such that A1: ( X is_>=_than a & ( 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; :: 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;
hence c = a by ORDERS_2:2; :: thesis: verum