let L be antisymmetric with_suprema RelStr ; :: thesis: for A being upper Subset of L
for B, C being Subset of L holds (A \/ B) "\/" (A \/ C) c= A \/ (B "\/" C)
let A be upper 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 <= x "\/" y by YELLOW_0:22;
A4: y <= x "\/" y by YELLOW_0:22;
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 20;
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 20;
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 20;
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;