let X be set ; :: thesis: for O1, O2 being Operation of X holds (O1 OR O2) AND (NOT O1) c= O2
let O1, O2 be Operation of X; :: thesis: (O1 OR O2) AND (NOT O1) c= O2
(O1 OR O2) AND (NOT O1) = (O1 AND (NOT O1)) OR (O2 AND (NOT O1)) by XBOOLE_1:23
.= {} \/ (O2 AND (NOT O1)) by Th52
.= O2 AND (NOT O1) ;
hence (O1 OR O2) AND (NOT O1) c= O2 by XBOOLE_1:17; :: thesis: verum