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;
A4: %I Y '<' PA by Th36;
A5: ERl (%I Y) c= ERl PA by A4, Th24;
A6: 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

A8: now

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

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

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

end;

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

thus z in ERl PA by A10; :: thesis: verum

end;

end;

end;

thus z in ERl PA by A8; :: thesis: verum

end;

A11: (id Y) \/ (ERl PA) c= ERl PA by A6, TARSKI:def 3;
A12: ERl PA c= (id Y) \/ (ERl PA) by XBOOLE_1:7;
A13: (id Y) \/ (ERl PA) = ERl PA by A11, A12, XBOOLE_0:def 10;
A14: PA '<' (%I Y) '\/' PA by A2, A3, A13, Th24;
A15: %I Y '<' PA by Th36;
A16: (%I Y) '\/' PA '<' PA by A15, Th33;
thus (%I Y) '\/' PA = PA by A14, A16, Th5; :: thesis: (%I Y) '/\' PA = %I Y
A17: 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 ;
thus (%I Y) '/\' PA = %I Y by A17, Th29; :: thesis: verum