set f = kappa_2 R;
for X, Y being Subset of R holds
( (kappa_2 R) . (X,Y) = 1 iff X c= Y )
proof
let X, Y be Subset of R; :: thesis: ( (kappa_2 R) . (X,Y) = 1 iff X c= Y )
thus ( (kappa_2 R) . (X,Y) = 1 implies X c= Y ) :: thesis: ( X c= Y implies (kappa_2 R) . (X,Y) = 1 )
proof
assume (kappa_2 R) . (X,Y) = 1 ; :: thesis: X c= Y
then kappa_2 (X,Y) = 1 by DefKappa2;
hence X c= Y by Prop11b; :: thesis: verum
end;
assume X c= Y ; :: thesis: (kappa_2 R) . (X,Y) = 1
then kappa_2 (X,Y) = 1 by Prop11b;
hence (kappa_2 R) . (X,Y) = 1 by DefKappa2; :: thesis: verum
end;
hence kappa_2 R is satisfying_RIF1 ; :: thesis: verum