let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
let G be Subset of (PARTITIONS Y); :: thesis: ( G is independent implies for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume A1: G is independent ; :: thesis: for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
let P, Q be Subset of (PARTITIONS Y); :: thesis: ( P c= G & Q c= G implies (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) )
assume ( P c= G & Q c= G ) ; :: thesis: (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
then ( (ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P)) & (ERl ('/\' Q)) * (ERl ('/\' P)) c= (ERl ('/\' P)) * (ERl ('/\' Q)) ) by A1, Lm1;
hence (ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P)) by XBOOLE_0:def 10; :: thesis: verum