set f = kappa_1 R;
for X, Y being Subset of R holds
( (kappa_1 R) . (X,Y) = 1 iff X c= Y )

proof

let X, Y be Subset of R; :: thesis: ( (kappa_1 R) . (X,Y) = 1 iff X c= Y )
thus ( (kappa_1 R) . (X,Y) = 1 implies X c= Y ) :: thesis: ( X c= Y implies (kappa_1 R) . (X,Y) = 1 )

proof

assume (kappa_1 R) . (X,Y) = 1 ; :: thesis: X c= Y
then kappa_1 (X,Y) = 1 by DefKappa1;
hence X c= Y by Prop11a; :: thesis: verum

end;

assume X c= Y ; :: thesis: (kappa_1 R) . (X,Y) = 1
then kappa_1 (X,Y) = 1 by Prop11a;
hence (kappa_1 R) . (X,Y) = 1 by DefKappa1; :: thesis: verum

end;

hence kappa_1 R is satisfying_RIF1 ; :: thesis: verum