let L be non empty RelStr ; :: thesis: for A, B, C being Subset of L holds A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)
let A, B, C be Subset of L; :: thesis: A "/\" (B \/ C) = (A "/\" B) \/ (A "/\" C)
thus A "/\" (B \/ C) c= (A "/\" B) \/ (A "/\" C) :: according to XBOOLE_0:def 10 :: thesis: (A "/\" B) \/ (A "/\" C) c= A "/\" (B \/ C)

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in A "/\" (B \/ C) or q in (A "/\" B) \/ (A "/\" C) )
assume q in A "/\" (B \/ C) ; :: thesis: q in (A "/\" B) \/ (A "/\" C)
then consider a, y being Element of L such that
A1: ( q = a "/\" y & a in A ) and
A2: y in B \/ C ;
( y in B or y in C ) by A2, XBOOLE_0:def 3;
then ( q in A "/\" B or q in A "/\" C ) by A1;
hence q in (A "/\" B) \/ (A "/\" C) by XBOOLE_0:def 3; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (A "/\" B) \/ (A "/\" C) or q in A "/\" (B \/ C) )
assume A3: q in (A "/\" B) \/ (A "/\" C) ; :: thesis: q in A "/\" (B \/ C)

per cases ( q in A "/\" B or q in A "/\" C ) by A3, XBOOLE_0:def 3;

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

then consider a, b being Element of L such that
A4: ( q = a "/\" b & a in A ) and
A5: b in B ;
b in B \/ C by A5, XBOOLE_0:def 3;
hence q in A "/\" (B \/ C) by A4; :: thesis: verum

end;

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

then consider a, b being Element of L such that
A6: ( q = a "/\" b & a in A ) and
A7: b in C ;
b in B \/ C by A7, XBOOLE_0:def 3;
hence q in A "/\" (B \/ C) by A6; :: thesis: verum

end;

end;