defpred S₁[ object , object ] means $1 = Bottom L;
consider R being Relation of the carrier of L, the carrier of L such that
A1: for a, b being object holds
( [a,b] in R iff ( a in the carrier of L & b in the carrier of L & S₁[a,b] ) ) from RELSET_1:sch 1();
reconsider R = R as Relation of L ;
take R ; :: thesis: for x, y being Element of L holds
( [x,y] in R iff x = Bottom L )
let x, y be Element of L; :: thesis: ( [x,y] in R iff x = Bottom L )
thus ( [x,y] in R implies x = Bottom L ) by A1; :: thesis: ( x = Bottom L implies [x,y] in R )
assume x = Bottom L ; :: thesis: [x,y] in R
hence [x,y] in R by A1; :: thesis: verum