defpred S_{1}[ 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 (PropRel Q)),(Class (PropRel Q)) such that

A1: for x, y being object holds

( [x,y] in R iff ( x in Class (PropRel Q) & y in Class (PropRel Q) & S_{1}[x,y] ) )
from RELSET_1:sch 1();

for B, C being Subset of (Prop Q) holds

( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) )_{1} being Relation of (Class (PropRel Q)) st

for B, C being Subset of (Prop Q) holds

( [B,C] in b_{1} iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) ) ; :: thesis: verum

( $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 (PropRel Q)),(Class (PropRel Q)) such that

A1: for x, y being object holds

( [x,y] in R iff ( x in Class (PropRel Q) & y in Class (PropRel Q) & S

for B, C being Subset of (Prop Q) holds

( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) )

proof

hence
ex b
let B, C be Subset of (Prop Q); :: thesis: ( [B,C] in R iff ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) ) :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) implies [B,C] in R )

p |- q ) ) ; :: thesis: [B,C] in R

hence [B,C] in R by A1; :: thesis: verum

end;p |- q ) ) )

thus ( [B,C] in R implies ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) ) :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( 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
( B in Class (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds
assume A2:
[B,C] in R
; :: thesis: ( B in Class (PropRel Q) & C in Class (PropRel Q) & ( 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 (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) by A1, A2; :: thesis: verum

end;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 (PropRel Q) & C in Class (PropRel Q) & ( for p, q being Element of Prop Q st p in B & q in C holds

p |- q ) ) by A1, A2; :: thesis: verum

p |- q ) ) ; :: thesis: [B,C] in R

hence [B,C] in R by A1; :: thesis: verum

for B, C being Subset of (Prop Q) holds

( [B,C] in b

p |- q ) ) ) ; :: thesis: verum