per cases ( not L is empty or L is empty ) ;

suppose A1: not L is empty ; :: thesis: id L is isomorphic

A2: id L = (id L) " by FUNCT_1:45;
id L is monotone ;
hence id L is isomorphic by A1, A2, WAYBEL_0:def 38; :: thesis: verum

end;

suppose L is empty ; :: thesis: id L is isomorphic

hence id L is isomorphic by WAYBEL_0:def 38; :: thesis: verum

end;

end;