let X, F, BB be set ; ( 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 }
; 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; ( [x,y] in F iff for c being set st c in BB & x c= c holds
y c= c )
hereby ( ( for c being set st c in BB & x c= c holds
y c= c ) implies [x,y] in F )
end;
assume
for c being set st c in BB & x c= c holds
y c= c
; [x,y] in F
hence
[x,y] in F
by A1; verum