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

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

( (%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

then A6:
(id Y) \/ (ERl PA) c= ERl PA
;
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

hence z in ERl PA ; :: thesis: verum

end;assume A5: z in (id Y) \/ (ERl PA) ; :: thesis: z in ERl PA

hence z in ERl PA ; :: thesis: verum

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