let R be non empty transitive antisymmetric with_infima RelStr ; :: thesis: for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
let x, y be Element of R; :: thesis: downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)

now

let z be set ; :: thesis: ( ( z in downarrow (x "/\" y) implies z in (downarrow x) /\ (downarrow y) ) & ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) ) )

hereby :: thesis: ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) )

assume A1: z in downarrow (x "/\" y) ; :: thesis: z in (downarrow x) /\ (downarrow y)
then reconsider z' = z as Element of R ;
A2: z' <= x "/\" y by A1, WAYBEL_0:17;
( x "/\" y <= x & x "/\" y <= y ) by YELLOW_0:23;
then ( z' <= x & z' <= y ) by A2, YELLOW_0:def 2;
then ( z' in downarrow x & z' in downarrow y ) by WAYBEL_0:17;
hence z in (downarrow x) /\ (downarrow y) by XBOOLE_0:def 4; :: thesis: verum

end;

assume A3: z in (downarrow x) /\ (downarrow y) ; :: thesis: z in downarrow (x "/\" y)
then A4: ( z in downarrow x & z in downarrow y ) by XBOOLE_0:def 4;
reconsider z' = z as Element of R by A3;
( z' <= x & z' <= y ) by A4, WAYBEL_0:17;
then x "/\" y >= z' by YELLOW_0:23;
hence z in downarrow (x "/\" y) by WAYBEL_0:17; :: thesis: verum

end;

hence downarrow (x "/\" y) = (downarrow x) /\ (downarrow y) by TARSKI:2; :: thesis: verum