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 Th27;
A2: ERl (%O Y) = nabla Y by Th37;
A3: (ERl (%O Y)) \/ (ERl PA) = ERl (%O Y) by A2, EQREL_1:1;
A4: ERl (%O Y) c= (ERl (%O Y)) "\/" (ERl PA) by A3, EQREL_1:def 3;
A5: %O Y '<' (%O Y) '\/' PA by A1, A4, Th24;
A6: %O Y '>' PA '\/' (%O Y) by Th36;
thus (%O Y) '\/' PA = %O Y by A5, A6, Th5; :: thesis: (%O Y) '/\' PA = PA
A7: ( ERl ((%O Y) '/\' PA) = (ERl (%O Y)) /\ (ERl PA) & ERl (%O Y) = nabla Y ) by Th28, Th37;
thus (%O Y) '/\' PA = PA by A7, Th29, XBOOLE_1:28; :: thesis: verum