let A, B be set ; :: thesis: for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let X1, X2 be Subset of A; :: thesis: for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let R be Subset of [:A,B:]; :: thesis: (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (R .:^ X1) \/ (R .:^ X2) or y in R .:^ (X1 /\ X2) )
assume A1: y in (R .:^ X1) \/ (R .:^ X2) ; :: thesis: y in R .:^ (X1 /\ X2)
A2: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then A3: (.: R) .: {_{(X1 /\ X2)}_} c= ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) by RELAT_1:121;
per cases ( y in R .:^ X1 or y in R .:^ X2 ) by A1, XBOOLE_0:def 3;
suppose A4: y in R .:^ X1 ; :: thesis: y in R .:^ (X1 /\ X2)
y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
proof
per cases ( (.: R) .: {_{(X1 /\ X2)}_} <> {} or (.: R) .: {_{(X1 /\ X2)}_} = {} ) ;
suppose A5: (.: R) .: {_{(X1 /\ X2)}_} <> {} ; :: thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
A6: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then A7: (.: R) .: {_{(X1 /\ X2)}_} c= ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) by RELAT_1:121;
A8: ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) <> {} by A5, A6, RELAT_1:121, XBOOLE_1:3;
(.: R) .: {_{X1}_} <> {} by A5, A7;
then A9: y in meet ((.: R) .: {_{X1}_}) by A4, SETFAM_1:def 9;
for Y being set st Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) holds
y in Y
proof
let Y be set ; :: thesis: ( Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) implies y in Y )
assume Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) ; :: thesis: y in Y
then Y in (.: R) .: {_{X1}_} by XBOOLE_0:def 4;
hence y in Y by A9, SETFAM_1:def 1; :: thesis: verum
end;
then y in meet (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A8, SETFAM_1:def 1;
then A10: y in Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A8, SETFAM_1:def 9;
Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) c= Intersect ((.: R) .: ({_{X1}_} /\ {_{X2}_})) by RELAT_1:121, SETFAM_1:44;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A2, A10; :: thesis: verum
end;
suppose (.: R) .: {_{(X1 /\ X2)}_} = {} ; :: thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then Intersect ((.: R) .: {_{(X1 /\ X2)}_}) = B by SETFAM_1:def 9;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A4; :: thesis: verum
end;
end;
end;
hence y in R .:^ (X1 /\ X2) ; :: thesis: verum
end;
suppose A11: y in R .:^ X2 ; :: thesis: y in R .:^ (X1 /\ X2)
y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
proof
per cases ( (.: R) .: {_{(X1 /\ X2)}_} <> {} or (.: R) .: {_{(X1 /\ X2)}_} = {} ) ;
suppose A12: (.: R) .: {_{(X1 /\ X2)}_} <> {} ; :: thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then A13: ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) <> {} by A2, RELAT_1:121, XBOOLE_1:3;
(.: R) .: {_{X2}_} <> {} by A3, A12;
then A14: y in meet ((.: R) .: {_{X2}_}) by A11, SETFAM_1:def 9;
for Y being set st Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) holds
y in Y
proof
let Y be set ; :: thesis: ( Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) implies y in Y )
assume Y in ((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_}) ; :: thesis: y in Y
then Y in (.: R) .: {_{X2}_} by XBOOLE_0:def 4;
hence y in Y by A14, SETFAM_1:def 1; :: thesis: verum
end;
then y in meet (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A13, SETFAM_1:def 1;
then A15: y in Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) by A13, SETFAM_1:def 9;
A16: {_{(X1 /\ X2)}_} = {_{X1}_} /\ {_{X2}_} by Th4;
Intersect (((.: R) .: {_{X1}_}) /\ ((.: R) .: {_{X2}_})) c= Intersect ((.: R) .: ({_{X1}_} /\ {_{X2}_})) by RELAT_1:121, SETFAM_1:44;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A15, A16; :: thesis: verum
end;
suppose (.: R) .: {_{(X1 /\ X2)}_} = {} ; :: thesis: y in Intersect ((.: R) .: {_{(X1 /\ X2)}_})
then Intersect ((.: R) .: {_{(X1 /\ X2)}_}) = B by SETFAM_1:def 9;
hence y in Intersect ((.: R) .: {_{(X1 /\ X2)}_}) by A11; :: thesis: verum
end;
end;
end;
hence y in R .:^ (X1 /\ X2) ; :: thesis: verum
end;
end;