let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for x being Element of L holds downarrow x = {x} "/\" ([#] L)
let x be Element of L; :: thesis: downarrow x = {x} "/\" ([#] L)
A1: {x} "/\" ([#] L) = { (x "/\" s) where s is Element of L : s in [#] L } by YELLOW_4:42;
thus downarrow x c= {x} "/\" ([#] L) :: according to XBOOLE_0:def 10 :: thesis: {x} "/\" ([#] L) c= downarrow x

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow x or q in {x} "/\" ([#] L) )
assume A2: q in downarrow x ; :: thesis: q in {x} "/\" ([#] L)
then reconsider q1 = q as Element of L ;
x >= q1 by A2, WAYBEL_0:17;
then x "/\" q1 = q1 by YELLOW_0:25;
hence q in {x} "/\" ([#] L) by A1; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} "/\" ([#] L) or q in downarrow x )
assume q in {x} "/\" ([#] L) ; :: thesis: q in downarrow x
then consider z being Element of L such that
A3: q = x "/\" z and
z in [#] L by A1;
x "/\" z <= x by YELLOW_0:23;
hence q in downarrow x by A3, WAYBEL_0:17; :: thesis: verum