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 :: thesis: for z being object holds
( ( z in downarrow (x "/\" y) implies z in (downarrow x) /\ (downarrow y) ) & ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) ) )

let z be object ; :: 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 z9 = z as Element of R ;
A2: z9 <= x "/\" y by A1, WAYBEL_0:17;
x "/\" y <= y by YELLOW_0:23;
then z9 <= y by A2, YELLOW_0:def 2;
then A3: z9 in downarrow y by WAYBEL_0:17;
x "/\" y <= x by YELLOW_0:23;
then z9 <= x by A2, YELLOW_0:def 2;
then z9 in downarrow x by WAYBEL_0:17;
hence z in (downarrow x) /\ (downarrow y) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume A4: z in (downarrow x) /\ (downarrow y) ; :: thesis: z in downarrow (x "/\" y)
then reconsider z9 = z as Element of R ;
z in downarrow y by A4, XBOOLE_0:def 4;
then A5: z9 <= y by WAYBEL_0:17;
z in downarrow x by A4, XBOOLE_0:def 4;
then z9 <= x by WAYBEL_0:17;
then x "/\" y >= z9 by A5, 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