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

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