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

proof

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

proof

assume (kappa R) . (X,Y) = 1 ; :: thesis: X c= Y
then kappa (X,Y) = 1 by DefKappa;
hence X c= Y by Prop1a; :: thesis: verum

end;

assume X c= Y ; :: thesis: (kappa R) . (X,Y) = 1
then kappa (X,Y) = 1 by Prop1a;
hence (kappa R) . (X,Y) = 1 by DefKappa; :: thesis: verum

end;

hence kappa R is satisfying_RIF1 ; :: thesis: verum