let L be reflexive antisymmetric with_suprema 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 ;
q1 <= q1 ;
then A3: q1 = q1 "\/" q1 by YELLOW_0:24;
( 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;