defpred S₁[ set ] means $1 is full infs-inheriting SubRelStr of L;
set SL = subrelstr ([#] L);
subrelstr ([#] L) is Element of (Sub L) by Def2;
then A1: subrelstr ([#] L) in the carrier of (Sub L) ;
A2: S₁[ subrelstr ([#] L)] ;
consider S being non empty strict full SubRelStr of Sub L such that
A3: for x being Element of (Sub L) holds
( x is Element of S iff S₁[x] ) from WAYBEL10:sch 1(A2, A1);
take S ; :: thesis: for R being strict SubRelStr of L holds
( R is Element of S iff ( R is infs-inheriting & R is full ) )
let R be strict SubRelStr of L; :: thesis: ( R is Element of S iff ( R is infs-inheriting & R is full ) )
R is Element of (Sub L) by Def2;
hence ( R is Element of S iff ( R is infs-inheriting & R is full ) ) by A3; :: thesis: verum