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