defpred S1[ object , object ] means ex B, C being Subset of (Prop Q) st
( \$1 = B & \$2 = C & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) );
consider R being Relation of (Class ()),(Class ()) such that
A1: for x, y being object holds
( [x,y] in R iff ( x in Class () & y in Class () & S1[x,y] ) ) from for B, C being Subset of (Prop Q) holds
( [B,C] in R iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )
proof
let B, C be Subset of (Prop Q); :: thesis: ( [B,C] in R iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) )

thus ( [B,C] in R implies ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) :: thesis: ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) implies [B,C] in R )
proof
assume A2: [B,C] in R ; :: thesis: ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) )

then ex B9, C9 being Subset of (Prop Q) st
( B = B9 & C = C9 & ( for p, q being Element of Prop Q st p in B9 & q in C9 holds
p |- q ) ) by A1;
hence ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) by A1, A2; :: thesis: verum
end;
assume ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ; :: thesis: [B,C] in R
hence [B,C] in R by A1; :: thesis: verum
end;
hence ex b1 being Relation of (Class ()) st
for B, C being Subset of (Prop Q) holds
( [B,C] in b1 iff ( B in Class () & C in Class () & ( for p, q being Element of Prop Q st p in B & q in C holds
p |- q ) ) ) ; :: thesis: verum