defpred S₁[ object , object ] means ex w1, w2 being Element of W st
( w1 = $1 & w2 = $2 & ( w1 <= w2 or w2 <= w1 ) );
ex R being Relation of the carrier of W st
for x, y being object holds
( [x,y] in R iff ( x in the carrier of W & y in the carrier of W & S₁[x,y] ) ) from RELSET_1:sch 1();
then consider R being Relation of the carrier of W such that
A1: for x, y being object holds
( [x,y] in R iff ( x in the carrier of W & y in the carrier of W & S₁[x,y] ) ) ;
take R ; :: thesis: for x, y being Element of W holds
( [x,y] in R iff ( x <= y or y <= x ) )
let x, y be Element of W; :: thesis: ( [x,y] in R iff ( x <= y or y <= x ) )
( [x,y] in R iff ( x in the carrier of W & y in the carrier of W & S₁[x,y] ) ) by A1;
hence ( [x,y] in R iff ( x <= y or y <= x ) ) ; :: thesis: verum