let X1, X2 be Subset-Family of Omega; :: thesis: ( ( for x being Subset of Omega holds
( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) & ( for x being Subset of Omega holds
( x in X2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ) implies X1 = X2 )
assume A2: for x being Subset of Omega holds
( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ; :: thesis: ( ex x being Subset of Omega st
( ( x in X2 implies ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) implies ( ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) & not x in X2 ) ) or X1 = X2 )
assume A3: for x being Subset of Omega holds
( x in X2 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) ; :: thesis: X1 = X2
now :: thesis: for x being Subset of Omega holds
( x in X1 iff x in X2 )
let x be Subset of Omega; :: thesis: ( x in X1 iff x in X2 )
( x in X1 iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st
( E c= J & x = meet (rng f) ) ) by A2;
hence ( x in X1 iff x in X2 ) by A3; :: thesis: verum
end;
hence X1 = X2 by SUBSET_1:3; :: thesis: verum