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