deffunc H₁( set ) -> set = $1;
let L1 be non empty finite reflexive transitive RelStr ; :: thesis: Ids L1 is finite
reconsider Y = bool the carrier of L1 as non empty finite set ;
A1: { X where X is Ideal of L1 : verum } c= { X where X is Element of Y : X is Ideal of L1 }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { X where X is Ideal of L1 : verum } or z in { X where X is Element of Y : X is Ideal of L1 } )
assume z in { X where X is Ideal of L1 : verum } ; :: thesis: z in { X where X is Element of Y : X is Ideal of L1 }
then ex X1 being Ideal of L1 st z = X1 ;
hence z in { X where X is Element of Y : X is Ideal of L1 } ; :: thesis: verum

end;

defpred S₁[ set ] means $1 is Ideal of L1;
A2: { X where X is Element of Y : X is Ideal of L1 } c= { X where X is Ideal of L1 : verum }

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { X where X is Element of Y : X is Ideal of L1 } or z in { X where X is Ideal of L1 : verum } )
assume z in { X where X is Element of Y : X is Ideal of L1 } ; :: thesis: z in { X where X is Ideal of L1 : verum }
then ex X1 being Element of Y st
( z = X1 & X1 is Ideal of L1 ) ;
hence z in { X where X is Ideal of L1 : verum } ; :: thesis: verum

end;

A3: { H₁(X) where X is Element of Y : S₁[X] } is finite from PRE_CIRC:sch 1();
Ids L1 = { X where X is Ideal of L1 : verum } by WAYBEL_0:def 23
.= { X where X is Element of Y : X is Ideal of L1 } by A1, A2, XBOOLE_0:def 10 ;
hence Ids L1 is finite by A3; :: thesis: verum