let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for A, B, C being Subset of L holds A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
let A, B, C be Subset of L; :: thesis: A \/ (B "/\" C) c= (A \/ B) "/\" (A \/ C)
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in A \/ (B "/\" C) or q in (A \/ B) "/\" (A \/ C) )
assume A1: q in A \/ (B "/\" C) ; :: thesis: q in (A \/ B) "/\" (A \/ C)
per cases ( q in A or q in B "/\" C ) by A1, XBOOLE_0:def 3;
suppose A2: q in A ; :: thesis: q in (A \/ B) "/\" (A \/ C)
then reconsider q1 = q as Element of L ;
A3: q1 = q1 "/\" q1 by YELLOW_0:25;
( q1 in A \/ B & q1 in A \/ C ) by A2, XBOOLE_0:def 3;
hence q in (A \/ B) "/\" (A \/ C) by A3; :: thesis: verum
end;
suppose q in B "/\" C ; :: thesis: q in (A \/ B) "/\" (A \/ C)
then consider b, c being Element of L such that
A4: q = b "/\" c and
A5: ( b in B & c in C ) ;
( b in A \/ B & c in A \/ C ) by A5, XBOOLE_0:def 3;
hence q in (A \/ B) "/\" (A \/ C) by A4; :: thesis: verum
end;
end;