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

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

hence
X1 = X2
by SUBSET_1:3; :: thesis: verum( 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;( 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