let R be non empty transitive antisymmetric with_infima RelStr ; :: thesis:
let x, y be Element of R; :: thesis:

let z be object ; :: thesis:

hereby :: thesis:

assume A1: z in downarrow (x "/\" y) ; :: thesis:
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:

end;

assume A4: z in (downarrow x) /\ (downarrow y) ; :: thesis:
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:

end;

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