reconsider X = F₂() as finite set by A1;
A4: X <> {} by A1;
defpred S₁[ object , object ] means ( not $1 in X or ( $2 in X & P₁[$1,$2] ) );
A5: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by A1, A3;
A6: for x, y being object holds
( S₁[x,y] or S₁[y,x] ) by A1, A2;
consider x being object such that
A7: x in X and
A8: for y being object st y in X holds
S₁[x,y] from CARD_2:sch 2(A4, A6, A5);
reconsider x = x as Element of F₁() by A1, A7;
take x ; :: thesis: ( x in F₂() & ( for y being Element of F₁() st y in F₂() holds
P₁[x,y] ) )
thus x in F₂() by A7; :: thesis: for y being Element of F₁() st y in F₂() holds
P₁[x,y]
let y be Element of F₁(); :: thesis: ( y in F₂() implies P₁[x,y] )
assume y in F₂() ; :: thesis: P₁[x,y]
hence P₁[x,y] by A7, A8; :: thesis: verum