let Y be non empty set ; :: thesis: for PA being a_partition of Y holds
( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )
let PA be a_partition of Y; :: thesis: ( (%I Y) '\/' PA = PA & (%I Y) '/\' PA = %I Y )
A1: ERl (%I Y) = id Y by Th38;
A2: ( ERl ((%I Y) '\/' PA) = (ERl (%I Y)) "\/" (ERl PA) & (ERl (%I Y)) \/ (ERl PA) c= (ERl (%I Y)) "\/" (ERl PA) ) by Th27, EQREL_1:def 3;
A3: (ERl (%I Y)) \/ (ERl PA) = (id Y) \/ (ERl PA) by Th38;
%I Y '<' PA by Th36;
then A5: ERl (%I Y) c= ERl PA by Th24;
for z being set st z in (id Y) \/ (ERl PA) holds
z in ERl PA

proof

let z be set ; :: thesis: ( z in (id Y) \/ (ERl PA) implies z in ERl PA )
assume A7: z in (id Y) \/ (ERl PA) ; :: thesis: z in ERl PA

now

per cases ( z in id Y or z in ERl PA ) by A7, XBOOLE_0:def 3;

case z in id Y ; :: thesis: z in ERl PA

hence z in ERl PA by A1, A5; :: thesis: verum

end;

case z in ERl PA ; :: thesis: z in ERl PA

hence z in ERl PA ; :: thesis: verum

end;

end;

end;

hence z in ERl PA ; :: thesis: verum

end;

then A11: (id Y) \/ (ERl PA) c= ERl PA by TARSKI:def 3;
ERl PA c= (id Y) \/ (ERl PA) by XBOOLE_1:7;
then (id Y) \/ (ERl PA) = ERl PA by A11, XBOOLE_0:def 10;
then A14: PA '<' (%I Y) '\/' PA by A2, A3, Th24;
%I Y '<' PA by Th36;
then (%I Y) '\/' PA '<' PA by Th33;
hence (%I Y) '\/' PA = PA by A14, Th5; :: thesis: (%I Y) '/\' PA = %I Y
ERl ((%I Y) '/\' PA) = (ERl (%I Y)) /\ (ERl PA) by Th28
.= (id Y) /\ (ERl PA) by Th38
.= id Y by EQREL_1:17
.= ERl (%I Y) by Th38 ;
hence (%I Y) '/\' PA = %I Y by Th29; :: thesis: verum