let X, F, BB be set ; :: thesis: ( F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } implies for x, y being Subset of X holds
( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c ) )
assume A1: F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } ; :: thesis: for x, y being Subset of X holds
( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c )
let x, y be Subset of X; :: thesis: ( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c )
hereby :: thesis: ( ( for c being set st c in BB & x c= c holds
y c= c ) implies [x,y] in F )
assume [x,y] in F ; :: thesis: for c being set st c in BB & x c= c holds
y c= c
then consider a, b being Subset of X such that
A2: [x,y] = [a,b] and
A3: for c being set st c in BB & a c= c holds
b c= c by A1;
A4: y = b by A2, XTUPLE_0:1;
x = a by A2, XTUPLE_0:1;
hence for c being set st c in BB & x c= c holds
y c= c by A3, A4; :: thesis: verum
end;
assume for c being set st c in BB & x c= c holds
y c= c ; :: thesis: [x,y] in F
hence [x,y] in F by A1; :: thesis: verum