set X = { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } ;
A1: the InternalRel of (subrelstr ({} L)) c= the InternalRel of L by YELLOW_0:def 13;
the carrier of (subrelstr ({} L)) = {} L by YELLOW_0:def 15;
then subrelstr ({} L) in { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } by A1;
then reconsider X = { RelStr(# A,B #) where A is Subset of L, B is Relation of A,A : B c= the InternalRel of L } as non empty set ;
defpred S1[ set , set ] means ex R being RelStr st
( $2 = R & $1 is SubRelStr of R );
consider S being non empty strict RelStr such that
A2: the carrier of S = X and
A3: for a, b being Element of S holds
( a <= b iff S1[a,b] ) from YELLOW_0:sch 1();
 take S ; :: thesis: ( ( for x being object holds
( x is Element of S iff x is strict SubRelStr of L ) ) & ( for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) )
hereby :: thesis: for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) )
let x be object ; :: thesis: ( ( x is Element of S implies x is strict SubRelStr of L ) & ( x is strict SubRelStr of L implies x is Element of S ) )
hereby :: thesis: ( x is strict SubRelStr of L implies x is Element of S )
assume x is Element of S ; :: thesis: x is strict SubRelStr of L
then x in X by A2;
then ex A being Subset of L ex B being Relation of A,A st
( x = RelStr(# A,B #) & B c= the InternalRel of L ) ;
hence x is strict SubRelStr of L by YELLOW_0:def 13; :: thesis: verum
end;
assume x is strict SubRelStr of L ; :: thesis: x is Element of S
then reconsider R = x as strict SubRelStr of L ;
A4: the InternalRel of R c= the InternalRel of L by YELLOW_0:def 13;
the carrier of R c= the carrier of L by YELLOW_0:def 13;
then R in X by A4;
hence x is Element of S by A2; :: thesis: verum
end;
thus for a, b being Element of S holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) by A3; :: thesis: verum