let Y be non empty set ; :: thesis: for PA being a_partition of Y holds
( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )
let PA be a_partition of Y; :: thesis: ( (%O Y) '\/' PA = %O Y & (%O Y) '/\' PA = PA )
A1: ERl ((%O Y) '\/' PA) = (ERl (%O Y)) "\/" (ERl PA) by Th23;
ERl (%O Y) = nabla Y by Th33;
then (ERl (%O Y)) \/ (ERl PA) = ERl (%O Y) by EQREL_1:1;
then ERl (%O Y) c= (ERl (%O Y)) "\/" (ERl PA) by EQREL_1:def 2;
then A2: %O Y '<' (%O Y) '\/' PA by A1, Th20;
%O Y '>' PA '\/' (%O Y) by Th32;
hence (%O Y) '\/' PA = %O Y by A2, Th4; :: thesis: (%O Y) '/\' PA = PA
( ERl ((%O Y) '/\' PA) = (ERl (%O Y)) /\ (ERl PA) & ERl (%O Y) = nabla Y ) by Th24, Th33;
hence (%O Y) '/\' PA = PA by Th25, XBOOLE_1:28; :: thesis: verum