let L be antisymmetric RelStr ; :: thesis: for a being Element of
for X being set holds
( a = "/\" X,L & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of st b is_<=_than X holds
a >= b ) ) )
let a be Element of ; :: thesis: for X being set holds
( a = "/\" X,L & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of st b is_<=_than X holds
a >= b ) ) )
let X be set ; :: thesis: ( a = "/\" X,L & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of st b is_<=_than X holds
a >= b ) ) )
( a is_<=_than X & ( for b being Element of st b is_<=_than X holds
a >= b ) implies ex_inf_of X,L ) by Th16;
hence ( a = "/\" X,L & ex_inf_of X,L iff ( a is_<=_than X & ( for b being Element of st b is_<=_than X holds
a >= b ) ) ) by Def10; :: thesis: verum