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 S_{1}[ 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 S_{1}[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 ) ) ) )

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) by A3; :: thesis: verum

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 S

( $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 S

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 ) )

thus
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 ) )

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;hereby :: thesis: ( x is strict SubRelStr of L implies x is Element of S )

assume
x is strict SubRelStr of L
; :: thesis: x is Element of Sassume
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;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

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

( a <= b iff ex R being RelStr st

( b = R & a is SubRelStr of R ) ) by A3; :: thesis: verum