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 Th34;
A2: ( ERl ((%I Y) '\/' PA) = (ERl (%I Y)) "\/" (ERl PA) & (ERl (%I Y)) \/ (ERl PA) c= (ERl (%I Y)) "\/" (ERl PA) ) by Th23, EQREL_1:def 2;
A3: (ERl (%I Y)) \/ (ERl PA) = (id Y) \/ (ERl PA) by Th34;
%I Y '<' PA by Th32;
then A4: ERl (%I Y) c= ERl PA by Th20;
for z being object st z in (id Y) \/ (ERl PA) holds
z in ERl PA
proof
let z be object ; :: thesis: ( z in (id Y) \/ (ERl PA) implies z in ERl PA )
assume A5: z in (id Y) \/ (ERl PA) ; :: thesis: z in ERl PA
now :: thesis: ( ( z in id Y & z in ERl PA ) or ( z in ERl PA & z in ERl PA ) )
per cases ( z in id Y or z in ERl PA ) by A5, XBOOLE_0:def 3;
case z in id Y ; :: thesis: z in ERl PA
hence z in ERl PA by A1, A4; :: 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 A6: (id Y) \/ (ERl PA) c= ERl PA ;
ERl PA c= (id Y) \/ (ERl PA) by XBOOLE_1:7;
then (id Y) \/ (ERl PA) = ERl PA by A6, XBOOLE_0:def 10;
then A7: PA '<' (%I Y) '\/' PA by A2, A3, Th20;
%I Y '<' PA by Th32;
then (%I Y) '\/' PA '<' PA by Th29;
hence (%I Y) '\/' PA = PA by A7, Th4; :: thesis: (%I Y) '/\' PA = %I Y
ERl ((%I Y) '/\' PA) = (ERl (%I Y)) /\ (ERl PA) by Th24
.= (id Y) /\ (ERl PA) by Th34
.= id Y by EQREL_1:10
.= ERl (%I Y) by Th34 ;
hence (%I Y) '/\' PA = %I Y by Th25; :: thesis: verum