let L be antisymmetric with_infima RelStr ; :: thesis: for A being lower Subset of L
for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let A be lower Subset of L; :: thesis: for B, C being Subset of L holds (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let B, C be Subset of L; :: thesis: (A \/ B) "/\" (A \/ C) c= A \/ (B "/\" C)
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (A \/ B) "/\" (A \/ C) or q in A \/ (B "/\" C) )
assume q in (A \/ B) "/\" (A \/ C) ; :: thesis: q in A \/ (B "/\" C)
then consider x, y being Element of L such that
A1: q = x "/\" y and
A2: ( x in A \/ B & y in A \/ C ) ;
A3: x "/\" y <= x by YELLOW_0:23;
A4: x "/\" y <= y by YELLOW_0:23;

per cases ( ( x in A & y in A ) or ( x in A & y in C ) or ( x in B & y in A ) or ( x in B & y in C ) ) by A2, XBOOLE_0:def 3;

suppose ( x in A & y in A ) ; :: thesis: q in A \/ (B "/\" C)

then q in A by A1, A3, WAYBEL_0:def 19;
hence q in A \/ (B "/\" C) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in A & y in C ) ; :: thesis: q in A \/ (B "/\" C)

then q in A by A1, A3, WAYBEL_0:def 19;
hence q in A \/ (B "/\" C) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in B & y in A ) ; :: thesis: q in A \/ (B "/\" C)

then q in A by A1, A4, WAYBEL_0:def 19;
hence q in A \/ (B "/\" C) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( x in B & y in C ) ; :: thesis: q in A \/ (B "/\" C)

then x "/\" y in B "/\" C ;
hence q in A \/ (B "/\" C) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;