A4:
for x, y being object st P1[x,y] & P1[y,x] holds
x = y
proof
let x,
y be
object ;
( P1[x,y] & P1[y,x] implies x = y )
reconsider x =
x,
y =
y as
set by TARSKI:1;
(
P1[
x,
y] &
P1[
y,
x] implies
x = y )
by A2;
hence
(
P1[
x,
y] &
P1[
y,
x] implies
x = y )
;
verum
end;
A5:
for x, y, z being object st P1[x,y] & P1[y,z] holds
P1[x,z]
proof
let x,
y,
z be
object ;
( P1[x,y] & P1[y,z] implies P1[x,z] )
reconsider x =
x,
y =
y,
z =
z as
set by TARSKI:1;
(
P1[
x,
y] &
P1[
y,
z] implies
P1[
x,
z] )
by A3;
hence
(
P1[
x,
y] &
P1[
y,
z] implies
P1[
x,
z] )
;
verum
end;
consider x being object such that
A6:
x in F1()
and
A7:
for y being object st y in F1() & y <> x holds
not P1[y,x]
from CARD_2:sch 1(A1, A4, A5);
reconsider x = x as set by TARSKI:1;
take
x
; ( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) )
thus
( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) )
by A6, A7; verum